saved
What TLA+ can and can't check
Hraness wrote this summary from a saved copy of the source. Quotations are taken word for word from the source.
gist
Hillel Wayne says TLA+, a temporal-logic language, checks invariants and liveness but cannot naturally express reachability or hyperproperties. He also limits it to properties stated as logical formulas over individual behaviors, while multi-step, real-time, floating-point, statistical, and vague human goals need workarounds or other formalisms. Those workarounds can distort models or enlarge their state spaces, so TLA+ remains useful without being universal.
ideas
- TLA+ checks safety and liveness properties over system behaviors. Invariants describe what remains true across states, action properties describe state changes, and composed temporal operators describe eventual outcomes.
- A property must be expressible as a logical formula before TLA+ can verify it. Human goals such as recognizing birds or keeping an application from being used to break the law may resist formalization.
- Several useful properties fall outside TLA+'s natural scope. The article names multi-step behavior, floating-point operations, real time, reachability, hyperproperties, statistical guarantees, and properties of the whole state space.
- Workarounds trade directness for complexity. Auxiliary variables, self-composition, REACHABLE, and TLCGet can mimic some missing properties, but they can damage refinements, enlarge the state space, or make models diverge from the system.
- Other formalisms cover some gaps without covering everything. The article points to Computation Tree Logic (CTL) for reachability and PRISM for probabilistic properties, with different tradeoffs from TLA+.
quotes
“to verify a property, we need to have a property to verify!”
“One single behavior isn't enough to cut it, so this is impossible to naturally check in TLA+.”
“These are useful hacks, but they're still hacks.”
“TLA+ is reasonably good at expressing and checking them.”