TLA+ (Temporal Logic of Actions) models a system as a set of behaviors, each behavior being a sequence of states. Using temporal operators, it can express invariants (e.g., []P meaning P holds in every state) and action properties such as [](x' >= x) (the new value of x is always at least the old value). Liveness properties, which assert that “something good always happens,” are built from the <> operator, examples including <>[]P (eventually P remains true forever) and P ~> Q (P leads to Q). These properties are evaluated across all possible behaviors, ensuring they hold universally.
A fundamental limitation is that TLA+ cannot express properties that require existential quantification over behaviors. For example, reachability properties like “there exists a behavior where P is true” — needed to prove a game is winnable — are outside the language’s scope. Similarly, TLA+ cannot express hyperproperties, which are properties over sets of behaviors; an example is verifying that an energy‑saving mode always uses less energy than normal mode across all possible action sequences, which would require comparing two distinct behaviors.
Although workarounds exist — such as using auxiliary variables to store a state history, employing self‑composition to model multiple behaviors, or leveraging the REACHABLE keyword and TLCGet in the TLC model checker — they introduce serious drawbacks. Auxiliary variables complicate refinements, self‑composition causes an exponential blow‑up of the state space, and these techniques often produce models that look messy and no longer correspond directly to the actual system. Other tools like CTL or PRISM can handle some of these properties but trade off by being weaker at the safety and liveness checks where TLA+ excels.