What TLA+ can and can't check
9 hours ago
- TLA+ is useful for verifying safety and liveness properties of concurrent systems, but it has limitations.
- Safety properties like invariants and action properties check that 'something bad never happens'.
- Liveness properties like '[]<>P' and '<>[]P' ensure 'something good eventually happens', such as termination or recovery.
- TLA+ cannot express properties that require multiple steps, floating-point operations, real time, or reachability.
- TLA+ cannot check existential properties (e.g., 'there exists a behavior where P is true') or hyperproperties (e.g., comparing two behaviors).
- Hyperproperties include security and statistical properties like 'energy saving mode uses less energy than normal mode'.
- Some limitations can be worked around with auxiliary variables, self-composition, or other tools, but these are complex hacks with drawbacks.
- TLA+ excels at many common invariants and liveness properties, but cannot express everything, so it's not a silver bullet for AI or software correctness.