I was reading Hillel Wayne’s new post TLA+ Won’t Solve Everything and became fixated on one of the things he says cannot be expressed in TLA⁺: Possibility and reachability properties: that it’s always possible to make P true, even if you don’t actually decide to. Things like “I can always shut down the computer” or “A user can always change their password”. These can’t be expressed with <>P because that’s “for all behaviors, P happens at least once”, we actually want “for all behavior prefixes, there is at least one behavior where P happens at least once”.