TLA+ is a formal specification language for describing systems, particularly concurrent and distributed ones. Created by Leslie Lamport, it’s built on simple mathematics: set theory and temporal logic. This foundation gives TLA+ remarkable expressive power while keeping the core language small.
This guide teaches TLA+ from scratch. You don’t need a math background, but it’ll help as things become more complex.
I’ll explain concepts as we go. By the end, you’ll be able to read and write TLA+ specifications.
Reading vs Writing TLA+: Reading specifications is easier than writing them. As you learn, focus first on understanding existing specs before trying to write your own. The examples throughout this guide are meant to be read carefully.
Set Theory Foundations
TLA+ is fundamentally based on set theory. Understanding sets is essential, they appear everywhere in specifications.
Basic Set Notation
Sets are collections of distinct elements:
{1, 2, 3} \* A set of integers
{"alice", "bob"} \* A set of strings
{TRUE, FALSE} \* The set of booleans (also written BOOLEAN)
{} \* The empty set
\in (in) and \notin (not in):
2 \in {1, 2, 3} \* TRUE
4 \notin {1, 2, 3} \* TRUE
Set Operations
{1, 2} \union {2, 3} \* {1, 2, 3} - union
{1, 2} \cap {2, 3} \* {2} - intersection
{1, 2, 3} \ {2} \* {1, 3} - set difference
{1, 2} \subseteq {1, 2, 3} \* TRUE - subset or equal
{1, 2} \subset {1, 2, 3} \* TRUE - proper subset
Set Constructors
Build sets from conditions or transformations:
\* Filter: elements of S satisfying predicate P
{x \in 1..10 : x > 5} \* {6, 7, 8, 9, 10}
\* Map: apply function f to each element
{x * 2 : x \in {1, 2, 3}} \* {2, 4, 6}
\* Combined: first filter, then map
{x * x : x \in {y \in 1..5 : y > 2}} \* {9, 16, 25}
Special Set Operations
SUBSET S \* Powerset: all subsets of S
UNION {{1,2}, {2,3}} \* Distributed union: {1, 2, 3}
Cardinality(S) \* Number of elements (requires FiniteSets)
S \X T \* Cartesian product: all pairs (s, t)
a..b creates {a, a+1, ..., b}.
Basic Operators and Expressions
Logical Operators
P /\ Q \* AND (conjunction)
P \/ Q \* OR (disjunction)
~P \* NOT (negation)
P => Q \* IMPLIES (if P then Q)
P <=> Q \* EQUIVALENT (P if and only if Q)
~, then /\ and \/ (same level), then <=>, then =>. Use parentheses when in doubt.
Comparison Operators
x = y \* Equality
x /= y \* Not equal (# is a synonym)
x < y \* Less than
x <= y \* Less than or equal
x > y \* Greater than
x >= y \* Greater than or equal
Arithmetic Operators
Requires EXTENDS Integers or EXTENDS Naturals:
x + y \* Addition
x - y \* Subtraction
x * y \* Multiplication
x \div y \* Integer division
x % y \* Modulo (remainder)
-x \* Negation
Conditional Expressions
IF condition THEN value1 ELSE value2
\* Example
IF x > 0 THEN "positive" ELSE "non-positive"
CASE x = 1 -> "one"
[] x = 2 -> "two"
[] x = 3 -> "three"
[] OTHER -> "other"
Local Definitions
LET-IN creates local bindings:
LET sum == x + y
product == x * y
IN sum * product
Quantifiers
Quantifiers make statements about sets of values.
Universal Quantification
\A means “for all”:
\* All elements of S satisfy P
\A x \in S : P(x)
\* Examples
\A n \in 1..10 : n > 0 \* TRUE: all positive
\A n \in 1..10 : n < 5 \* FALSE: 5..10 aren't < 5
Existential Quantification
\E means “there exists”:
\* Some element of S satisfies P
\E x \in S : P(x)
\* Examples
\E n \in 1..10 : n > 5 \* TRUE: 6, 7, 8, 9, 10 qualify
\E n \in 1..10 : n > 100 \* FALSE: none qualify
The CHOOSE Operator
CHOOSE picks an arbitrary element satisfying a condition:
CHOOSE x \in S : P(x)
\* Example: pick any even number from 1..10
CHOOSE n \in 1..10 : n % 2 = 0 \* Could be 2, 4, 6, 8, or 10
CHOOSE always returns the same value for identical inputs within a model run—it’s deterministic in that sense. However, the specification doesn’t define which qualifying value it picks. Your specification shouldn’t depend on a particular choice.
Bounded vs Unbounded
Always use bounded quantifiers (\A x \in S) rather than unbounded (\A x). Unbounded quantifiers can’t be model-checked and should only appear in proofs.
Functions and Records
Functions in TLA+ map elements from a domain to values.
Function Definition
\* Function mapping each x in S to expression e
[x \in S |-> e]
\* Examples
[n \in 1..3 |-> n * n] \* Maps 1->1, 2->4, 3->9
[acct \in {"alice", "bob"} |-> 0] \* Maps "alice"->0, "bob"->0
Function Application
f[x] \* Apply function f to argument x
\* Example
LET square == [n \in 1..10 |-> n * n]
IN square[5] \* Returns 25
DOMAIN
DOMAIN f \* The set of valid arguments to f
\* Example
LET f == [n \in 1..3 |-> n * 2]
IN DOMAIN f \* Returns {1, 2, 3}
Updating Functions with EXCEPT
EXCEPT creates a new function with some values changed:
[f EXCEPT ![a] = b] \* f with f[a] changed to b
\* Example: bank account update
LET balance == [acct \in {"alice", "bob"} |-> 100]
IN [balance EXCEPT !["alice"] = 150] \* Alice now has 150, Bob still 100
[f EXCEPT ![a] = b, ![c] = d]
\* Using @ to reference old value
[balance EXCEPT !["alice"] = @ + 50] \* Add 50 to Alice's balance
Records
Records are functions with string domains:
[name |-> "Alice", age |-> 30] \* A record
\* Access with dot notation
record.name \* "Alice"
record["name"] \* Also "Alice"
\* Update with EXCEPT
[record EXCEPT !.age = 31] \* Birthday!
Sequences
Sequences are functions with domain 1..n. Requires EXTENDS Sequences:
<<1, 2, 3>> \* A sequence of length 3
Len(seq) \* Length
Head(seq) \* First element
Tail(seq) \* All but first
Append(seq, x) \* Add x to end
seq1 \o seq2 \* Concatenation
MODULE Structure
TLA+ specifications are organized into modules.
---------------------------- MODULE ModuleName ----------------------------
\* This line and the === line below are the module delimiters
EXTENDS Integers, Sequences, FiniteSets
\* Import standard modules
CONSTANTS MaxValue, Nodes
\* Parameters set when running the model checker
ASSUME MaxValue > 0 /\ MaxValue \in Nat
\* Assumptions about constants
VARIABLES x, y, z
\* State variables
\* Operator definitions go here...
=============================================================================
\* End of module
\* Single-line comment
(* Multi-line
comment *)
EXTENDS
Standard modules provide common operations:
| Module | Provides |
|---|
Integers | Integer arithmetic, Int set |
Naturals | Natural numbers, Nat set |
Sequences | Sequence operations |
FiniteSets | Cardinality, IsFiniteSet |
TLC | Model checker utilities |
Defining Operators
Operators are like functions or macros—they name expressions for reuse.
Simple Definitions
Max(a, b) == IF a > b THEN a ELSE b
IsEmpty(S) == S = {}
Adults == {p \in People : p.age >= 18}
Recursive Operators
RECURSIVE Factorial(_)
Factorial(n) == IF n = 0 THEN 1 ELSE n * Factorial(n - 1)
RECURSIVE Sum(_)
Sum(S) == IF S = {} THEN 0
ELSE LET x == CHOOSE x \in S : TRUE
IN x + Sum(S \ {x})
Higher-Order Operators
Operators can take other operators as arguments:
Apply(Op(_), x) == Op(x)
MapSet(Op(_), S) == {Op(x) : x \in S}
State and Actions
A state is a snapshot of your system at a moment in time, specifically, the values assigned to all variables. A behavior is a sequence of states, showing how your system evolves over time. TLA+ models systems by describing valid initial states and valid transitions between states.
Prime Notation
The prime symbol (') refers to the value in the next state:
x' = x + 1 \* In the next state, x equals current x plus 1
A Simple Example: Counter
VARIABLE counter
Init == counter = 0
Increment == counter' = counter + 1
Decrement == counter > 0 /\ counter' = counter - 1
Init defines the initial state. Increment and Decrement are actions, each describes a valid state transition.
UNCHANGED
When an action doesn’t modify a variable, say so explicitly:
VARIABLES x, y
IncrementX ==
/\ x' = x + 1
/\ UNCHANGED y \* y stays the same
\* Equivalent to:
\* /\ x' = x + 1
\* /\ y' = y
Enabling Conditions
Actions often have preconditions (guards):
Decrement ==
/\ counter > 0 \* Enabling condition: can only decrement if > 0
/\ counter' = counter - 1
counter > 0.
The vars Tuple Pattern
Group all variables into a tuple for convenience:
VARIABLES x, y, z
vars == <<x, y, z>>
Init and Next
The standard pattern for behavioral specifications:
Init ==
/\ x = 0
/\ y = 0
Next ==
\/ IncrementX
\/ IncrementY
\/ Reset
\* The complete specification
Spec == Init /\ [][Next]_vars
Next is a disjunction of all possible actions. The system can take any enabled action at each step.
Bank Transfer Example
VARIABLES balance
Init == balance = [acct \in {"alice", "bob"} |-> 100]
Transfer(from, to, amount) ==
/\ balance[from] >= amount \* Guard: sufficient funds
/\ balance' = [balance EXCEPT
![from] = @ - amount,
![to] = @ + amount]
Next == \E from, to \in DOMAIN balance :
\E amt \in 1..balance[from] :
/\ from /= to
/\ Transfer(from, to, amt)
Temporal Operators
TLA+ can express properties about behavior over time.
Always (Box)
[]P means P holds in every state of every behavior:
[]TypeOK \* TypeOK is always true
[](balance >= 0) \* Balance is never negative
Eventually (Diamond)
<>P means P holds in some future state:
<>Done \* The system eventually terminates
<>(x = 0) \* x eventually becomes zero
Combining Temporal Operators
[]<>P \* P holds infinitely often
<>[]P \* P eventually holds forever
Leads-To
P ~> Q means whenever P holds, Q eventually follows:
Request ~> Response \* Every request gets a response
(x = 0) ~> (x > 0) \* If x is 0, it eventually becomes positive
[Next]_vars means “either Next happens, or nothing changes”:
[Next]_vars == Next \/ (vars' = vars)
Spec == Init /\ [][Next]_vars
Safety vs Liveness
Safety properties say “bad things never happen”:
[](balance >= 0) — balance never goes negative[]MutualExclusion — two processes never in critical section
Liveness properties say “good things eventually happen”:
<>Terminated — system eventually terminatesRequest ~> Response — requests get responses
Safety can be checked directly. Liveness requires fairness assumptions—telling the model checker that enabled actions eventually execute.
Type Correctness and Invariants
The TypeOK Pattern
Define valid states with a type invariant:
TypeOK ==
/\ balance \in [{"alice", "bob"} -> Nat]
/\ counter \in 0..100
/\ status \in {"idle", "running", "done"}
[S -> T] means “the set of all functions from S to T.” So balance \in [{"alice", "bob"} -> Nat] says balance is a function mapping account names to natural numbers.
TypeOK should be an invariant: []TypeOK.
Writing Invariants
Invariants are safety properties, conditions that must always hold:
\* No account goes negative
NoOverdraft == \A acct \in DOMAIN balance : balance[acct] >= 0
\* Total money is conserved (for a two-account system)
TotalConserved ==
balance["alice"] + balance["bob"] = 200
\* At most one process in critical section
MutualExclusion == Cardinality(inCS) <= 1
Complete Specification: Mutex
Here’s a complete, runnable specification for mutual exclusion:
------------------------------ MODULE Mutex --------------------------------
EXTENDS Integers, FiniteSets
CONSTANT Procs \* Set of processes
VARIABLES
waiting, \* Processes waiting to enter
inCS \* Processes in critical section
vars == <<waiting, inCS>>
TypeOK ==
/\ waiting \subseteq Procs
/\ inCS \subseteq Procs
MutualExclusion ==
Cardinality(inCS) <= 1 \* At most one in CS
Init ==
/\ waiting = {}
/\ inCS = {}
Request(p) ==
/\ p \notin waiting
/\ p \notin inCS
/\ waiting' = waiting \union {p}
/\ UNCHANGED inCS
Enter(p) ==
/\ p \in waiting
/\ inCS = {} \* CS must be empty
/\ waiting' = waiting \ {p}
/\ inCS' = {p}
Exit(p) ==
/\ p \in inCS
/\ inCS' = {}
/\ UNCHANGED waiting
Next ==
\E p \in Procs :
\/ Request(p)
\/ Enter(p)
\/ Exit(p)
Spec == Init /\ [][Next]_vars
\* Properties to verify
THEOREM Spec => []TypeOK
THEOREM Spec => []MutualExclusion
=============================================================================
CONSTANT Procs = {p1, p2, p3}
INVARIANT TypeOK
INVARIANT MutualExclusion
Standard Modules Reference
| Module | Key Operations |
|---|
Integers | Int, +, -, *, \div, %, .. |
Naturals | Nat, same arithmetic (non-negative only) |
Sequences | Seq(S), Len, Head, Tail, Append, \o, SubSeq |
FiniteSets | Cardinality, IsFiniteSet |
TLC | Print, Assert, @@, :> (for model checking) |
Bags | Multisets (bags) operations |
Running Specifications
Configuration Files
A .cfg file tells TLC what to check:
CONSTANTS
MaxValue = 10
Procs = {p1, p2}
INIT Init
NEXT Next
INVARIANT TypeOK
INVARIANT SafetyProperty
PROPERTY LivenessProperty
- Write your
.tla specification
- Create a
.cfg configuration
- Run TLC (the model checker)
- If an invariant fails, TLC shows the counterexample trace
See MacTLA for native macOS verification or the TLA+ Toolbox for cross-platform.
Common Patterns and Idioms
The vars Tuple
Always define a vars tuple grouping all variables:
vars == <<x, y, z>>
\* Then use in Spec
Spec == Init /\ [][Next]_vars
Guard-Action Pattern
Structure actions as guard (enabling condition) + effect:
DoSomething ==
/\ guard1 \* Preconditions
/\ guard2
/\ x' = newValue1 \* State changes
/\ y' = newValue2
/\ UNCHANGED otherVars
Helper Operators
Extract common logic into named operators:
CanTransfer(from, amount) ==
/\ from \in DOMAIN balance
/\ balance[from] >= amount
/\ amount > 0
Transfer(from, to, amount) ==
/\ CanTransfer(from, amount)
/\ from /= to
/\ balance' = [balance EXCEPT ![from] = @ - amount, ![to] = @ + amount]
Sets vs Sequences
- Use sets when order doesn’t matter and duplicates aren’t allowed
- Use sequences when order matters or you need duplicates
\* Set: processes waiting (order irrelevant)
waiting \subseteq Procs
\* Sequence: message queue (order matters)
queue \in Seq(Messages)
What to Read Next
Domain-specific examples:
Tools:
- MacTLA — native macOS verification with TLC and TLAPS, I wrote it
External resources: