Can we have reachability properties in TLA⁺?
Summary
The post analyzes how reachability properties can be expressed and checked in TLA+. It covers the ENABLED operator, basic and full reachability, backward reachability, and the use of machine-closed fairness assumptions to derive reachability results, ending with a practical takeaway that TLC can support such checks via (Spec ∧ F) ⇒ □◇P.