A general rule-of-thumb in TLA+ is "default is worst-case". If you don't explicitly declare your actions are fair, they'll be unfair. If you don't explicitly encode atomicity into your spec, it's not atomic.

Much better to accidentally get a false positive than a false negative.