TLA+ Syntax and Usage Guide

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.

If you want to run specifications, grab MacTLA (native macOS, I wrote it) or the TLA+ Toolbox (cross-platform). For domain-specific examples, see the AD Tier Model specification or aviation systems models.

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

Membership is tested with \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)

The range notation 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)

Precedence (highest to lowest): ~, 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 expressions for multiple conditions:

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

Multiple updates:

[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

Comments

\* 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

An action is a formula containing primed and unprimed variables. It describes how state changes.

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

The action is only enabled when counter > 0.

The vars Tuple Pattern

Group all variables into a tuple for convenience:

VARIABLES x, y, z
vars == <<x, y, z>>

This simplifies temporal formulas (explained below).

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

Stuttering and the Spec Formula

A stuttering step is one where nothing changes. Real systems can stutter (e.g., waiting for I/O). The notation [Next]_vars means “either Next happens, or nothing changes”:

[Next]_vars  ==  Next \/ (vars' = vars)

The standard specification form:

Spec == Init /\ [][Next]_vars

This says: start in an Init state, then repeatedly take Next steps (or stutter).

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 terminates
Request ~> 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"}

The notation [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
=============================================================================

To run this, create a configuration file (Mutex.cfg):

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

Using MacTLA or TLA+ Toolbox

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)

​Set Theory Foundations

​Basic Set Notation

​Set Operations

​Set Constructors

​Special Set Operations

​Basic Operators and Expressions

​Logical Operators

​Comparison Operators

​Arithmetic Operators

​Conditional Expressions

​Local Definitions

​Quantifiers

​Universal Quantification

​Existential Quantification

​The CHOOSE Operator

​Bounded vs Unbounded

​Functions and Records

​Function Definition

​Function Application

​DOMAIN

​Updating Functions with EXCEPT

​Records

​Sequences

​MODULE Structure

​Comments

​EXTENDS

​Defining Operators

​Simple Definitions

​Recursive Operators

​Higher-Order Operators

​State and Actions

​Prime Notation

​A Simple Example: Counter

​UNCHANGED

​Enabling Conditions

​The vars Tuple Pattern

​Init and Next

​Bank Transfer Example

​Temporal Operators

​Always (Box)

​Eventually (Diamond)

​Combining Temporal Operators

​Leads-To

​Stuttering and the Spec Formula

​Safety vs Liveness

​Type Correctness and Invariants

​The TypeOK Pattern

​Writing Invariants

​Complete Specification: Mutex

​Standard Modules Reference

​Running Specifications

​Configuration Files

​Using MacTLA or TLA+ Toolbox

​Common Patterns and Idioms

​The vars Tuple

​Guard-Action Pattern

​Helper Operators

​Sets vs Sequences

​What to Read Next

Set Theory Foundations

Basic Set Notation

Set Operations

Set Constructors

Special Set Operations

Basic Operators and Expressions

Logical Operators

Comparison Operators

Arithmetic Operators

Conditional Expressions

Local Definitions

Quantifiers

Universal Quantification

Existential Quantification

The CHOOSE Operator

Bounded vs Unbounded

Functions and Records

Function Definition

Function Application

DOMAIN

Updating Functions with EXCEPT

Records

Sequences

MODULE Structure

Comments

EXTENDS

Defining Operators

Simple Definitions

Recursive Operators

Higher-Order Operators

State and Actions

Prime Notation

A Simple Example: Counter

UNCHANGED

Enabling Conditions

The vars Tuple Pattern

Init and Next

Bank Transfer Example

Temporal Operators

Always (Box)

Eventually (Diamond)

Combining Temporal Operators

Leads-To

Stuttering and the Spec Formula

Safety vs Liveness

Type Correctness and Invariants

The TypeOK Pattern

Writing Invariants

Complete Specification: Mutex

Standard Modules Reference

Running Specifications

Configuration Files

Using MacTLA or TLA+ Toolbox

Common Patterns and Idioms

The vars Tuple

Guard-Action Pattern

Helper Operators

Sets vs Sequences

What to Read Next