TLA+ (Temporal Logic of Actions)

Origin. Leslie Lamport (1990s). Concurrent systems. Actions as formulas. Stuttering invariance. Foundation of distributed systems verification.

Models. States and actions. Temporal logic over behaviors. Stuttering equivalence. Refinement mapping. Specification of concurrent systems.

Formalism.

State and action: State: assignment to variables. Action: relation between states (primed/unprimed). x' = x + 1: action updating x. Enabled(A): action can occur.

Behavior: σ = s₀ → s₁ → s₂ → ... Infinite sequence of states. Behavior satisfies formula. Model of specification.

Temporal operators: □P: always P. ◇P: eventually P. P ⇝ Q: P leads to Q, defined as □(P ⇒ ◇Q). Not ⊢, which is entailment and not a TLA+ operator. □[A]_v: stuttering action.

Stuttering: □[A]_v ≡ □(A ∨ v' = v). Allow steps where v unchanged. Stuttering equivalence. Refinement basis.

Specification form: Init ∧ □[Next]_vars ∧ Fairness. Initial condition. Next-state relation. Fairness: liveness.

Fairness: WF_v(A): weak fairness (if enabled forever, occurs). SF_v(A): strong fairness (if enabled infinitely, occurs). Liveness constraints.

TLC model checker: Exhaustive state exploration. Finite-state abstraction. Error traces. Parallel checking.

Symbols.

Symbol	Unicode	Name	Meaning
'	U+0027	Apostrophe / Priming	x' is the value of x in the next state of a step
□	U+25A1	White square / Always	Holds at every position of the behaviour
◇	U+25C7	White diamond / Eventually	Holds at some position
⇝	U+21DD	Squiggle right arrow / Leads to	P ⇝ Q, defined as □(P ⇒ ◇Q)
⇒	U+21D2	Rightwards double arrow / Implication	Inside the definition of ⇝
≡	U+2261	Identical to / Definitional equality	□[A]_v ≡ □(A ∨ v' = v)
∧	U+2227	Logical and	Conjoins Init, □[Next]_vars, and fairness
∨	U+2228	Logical or	The stuttering disjunct A ∨ v' = v
=	U+003D	Equals sign	v' = v, the stuttering step
[A]_v	—	Stuttering action	A or a step leaving v unchanged
σ	U+03C3	Sigma / Behaviour	The infinite state sequence s₀ → s₁ → …
WF_v(A)	—	Weak fairness	If A is continuously enabled, an A step occurs
SF_v(A)	—	Strong fairness	If A is repeatedly enabled, an A step occurs
Enabled	—	Enabledness predicate	Holds where the action can be taken
Init, Next	—	Specification parts	Initial predicate and next-state relation
TLC	—	Model checker	Explicit-state exhaustive checker for TLA+

Metatheory. The design decision that organizes everything else is that a specification is a single formula of a temporal logic, so implementation is implication: system S implements specification T exactly when ⊨ S ⇒ T, and refinement needs no separate relation. Making this work requires that no formula distinguish behaviours differing only by repeated states, which is why the next-state relation is always written □[Next]_vars rather than □Next — the bracket admits stuttering steps, and stuttering invariance is what allows a low-level specification with more steps to imply a high-level one with fewer. Lamport's TLA (1994) restricts the temporal operators severely: □ and ◇ apply to actions and state predicates but arbitrary nesting of temporal operators inside actions is excluded, which keeps the logic usable for refinement while retaining enough power for liveness through the fairness operators WF and SF. Alpern and Schneider's decomposition sits underneath the specification form: Init ∧ □[Next]_vars is the safety part and the fairness conjuncts are the liveness part. TLC decides properties by exhaustive exploration of a finite instance; TLAPS discharges proofs of the general case.

Applies to. Distributed systems. Concurrent algorithms. Protocols. Amazon use.

Limitations. The logic is expressive enough to be undecidable: TLA+ takes untyped Zermelo–Fraenkel set theory as its data language, so validity is not merely undecidable but unaxiomatizable, and every proof beyond a finite instance is human-directed. TLC does not check a specification but a finite instantiation of one — bounded message counts, bounded process counts, bounded values — so success establishes the property for that instance only, and a violation appearing at five processes but not three is invisible. Stuttering invariance, which gives refinement, forecloses anything a stuttering step can affect: real-time properties and step-counting are not expressible, since the logic cannot tell a behaviour from one with extra idling. Probability is likewise outside the assertion language, so randomized protocols can be specified only through their nondeterministic abstraction. Refinement by implication requires a refinement mapping, and one need not exist without adding history or prophecy variables.