What TLA+ can and can't check

TLA+ models systems as sets of behaviors, where each behavior is a sequence of states and properties are boolean formulas over those states combined with temporal operators: always (P true now and forever), prime (P in the next state), and eventually (P true now or at some future state). Invariants are properties true in every state of every behavior; action properties combine current and next-state predicates and together with invariants form safety guarantees ("something bad never happens"). Liveness properties use eventually and compositions like leads-to (P ~> Q) to assert that good things will occur or persist, and refinement composes safety and liveness to relate specifications to implementations.

Key limitations are structural: a property must be formalizable as a temporal formula over individual behaviors, so existential reachability ("there exists a behavior where P") is not native, nor are hyperproperties that compare multiple behaviors, multi-step properties expressed only in terms of single-step actions, real-time or floating-point semantics, or certain global metaproperties over the state space. Workarounds - auxiliary history variables, self-composition, TLC’s REACHABLE/TLCGet - can encode some missing checks but break refinements, explode state space, and lead to unnatural specs. Other logics and tools (e.g., CTL, probabilistic model checkers) cover some gaps but trade away strengths TLA+ offers. TLA+ excels at many concurrency invariants and liveness proofs but is not a universal solution for every verification need.