TLA+

TLA+ (Temporal Logic of Actions) is a formal specification language developed by Leslie Lamport for describing concurrent and distributed systems. Unlike programming languages, TLA+ is not designed for execution but for reasoning: it allows engineers to write precise, unambiguous specifications of system behavior and to prove properties about those specifications using model checking or proof.

The language is built on a foundation of temporal logic and set theory. A TLA+ specification describes a system as a set of possible behaviors — infinite sequences of states — where each state assigns values to variables. The core construct is the action: a predicate relating a current state to a next state, written using primed variables (x' denotes the value of x in the next state). This simple notation captures all forms of state transition, from assignment to non-determinism to stuttering (where variables do not change).

TLA+ has been used in industry to find design bugs before implementation begins. Amazon Web Services used TLA+ to verify the correctness of several distributed algorithms, including parts of S3 and DynamoDB, finding subtle bugs that would have been expensive to fix after deployment. The language's power lies not in generating code but in forcing engineers to think precisely about what they are building before they build it.

TLA+ is supported by the TLC model checker, which exhaustively searches finite-state instances for property violations, and the TLAPS proof system, which can verify properties using formal proof. The language is notable for its minimalism: a small number of constructs, a simple semantics, and a focus on specification over implementation.

TLA+ is the specification language that software engineers deserve but rarely use. Its minimalism is a discipline: it forces the engineer to confront the gap between what they think their system does and what it actually does. The reason TLA+ has not spread beyond its niche is not that it is difficult — it is that it is honest. Most software engineering cultures prefer optimism to honesty, and they pay for that preference in production incidents. TLA+ will not prevent all bugs. It prevents the bugs that arise from not knowing what you meant.