> ## Documentation Index
> Fetch the complete documentation index at: https://docs.alchemicalchef.io/llms.txt
> Use this file to discover all available pages before exploring further.

# TLA+ Syntax and Usage Guide

> A comprehensive introduction to TLA+ syntax, from set theory foundations to temporal logic and complete specifications

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.

<Tip>
  **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.
</Tip>

If you want to run specifications, grab [MacTLA](/formal-methods/mactla) (native macOS, I wrote it) or the [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html) (cross-platform). For domain-specific examples, see the [AD Tier Model specification](/formal-methods/tla-specification) or [aviation systems models](/formal-methods/aviation-formal-methods-part1).

## 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:

```tla theme={null}
{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):

```tla theme={null}
2 \in {1, 2, 3}              \* TRUE
4 \notin {1, 2, 3}           \* TRUE
```

### Set Operations

```tla theme={null}
{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:

```tla theme={null}
\* 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

```tla theme={null}
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

```tla theme={null}
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

```tla theme={null}
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`:

```tla theme={null}
x + y            \* Addition
x - y            \* Subtraction
x * y            \* Multiplication
x \div y         \* Integer division
x % y            \* Modulo (remainder)
-x               \* Negation
```

### Conditional Expressions

```tla theme={null}
IF condition THEN value1 ELSE value2

\* Example
IF x > 0 THEN "positive" ELSE "non-positive"
```

CASE expressions for multiple conditions:

```tla theme={null}
CASE x = 1 -> "one"
  [] x = 2 -> "two"
  [] x = 3 -> "three"
  [] OTHER -> "other"
```

### Local Definitions

LET-IN creates local bindings:

```tla theme={null}
LET sum == x + y
    product == x * y
IN sum * product
```

## Quantifiers

Quantifiers make statements about sets of values.

### Universal Quantification

`\A` means "for all":

```tla theme={null}
\* 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":

```tla theme={null}
\* 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:

```tla theme={null}
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
```

<Info>
  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.
</Info>

### 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

```tla theme={null}
\* 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

```tla theme={null}
f[x]                                  \* Apply function f to argument x

\* Example
LET square == [n \in 1..10 |-> n * n]
IN square[5]                          \* Returns 25
```

### DOMAIN

```tla theme={null}
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:

```tla theme={null}
[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:

```tla theme={null}
[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:

```tla theme={null}
[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`:

```tla theme={null}
<<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.

```tla theme={null}
---------------------------- 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

```tla theme={null}
\* 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

```tla theme={null}
Max(a, b) == IF a > b THEN a ELSE b

IsEmpty(S) == S = {}

Adults == {p \in People : p.age >= 18}
```

### Recursive Operators

```tla theme={null}
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:

```tla theme={null}
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:

```tla theme={null}
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

```tla theme={null}
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:

```tla theme={null}
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):

```tla theme={null}
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:

```tla theme={null}
VARIABLES x, y, z
vars == <<x, y, z>>
```

This simplifies temporal formulas (explained below).

### Init and Next

The standard pattern for behavioral specifications:

```tla theme={null}
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

```tla theme={null}
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:

```tla theme={null}
[]TypeOK                     \* TypeOK is always true
[](balance >= 0)             \* Balance is never negative
```

### Eventually (Diamond)

`<>P` means P holds in *some* future state:

```tla theme={null}
<>Done                       \* The system eventually terminates
<>(x = 0)                    \* x eventually becomes zero
```

### Combining Temporal Operators

```tla theme={null}
[]<>P                        \* P holds infinitely often
<>[]P                        \* P eventually holds forever
```

### Leads-To

`P ~> Q` means whenever P holds, Q eventually follows:

```tla theme={null}
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":

```tla theme={null}
[Next]_vars  ==  Next \/ (vars' = vars)
```

The standard specification form:

```tla theme={null}
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:

```tla theme={null}
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:

```tla theme={null}
\* 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:

```tla theme={null}
------------------------------ 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

1. Write your `.tla` specification
2. Create a `.cfg` configuration
3. Run TLC (the model checker)
4. If an invariant fails, TLC shows the counterexample trace

See [MacTLA](/formal-methods/mactla) for native macOS verification or the [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html) for cross-platform.

## Common Patterns and Idioms

### The vars Tuple

Always define a vars tuple grouping all variables:

```tla theme={null}
vars == <<x, y, z>>

\* Then use in Spec
Spec == Init /\ [][Next]_vars
```

### Guard-Action Pattern

Structure actions as guard (enabling condition) + effect:

```tla theme={null}
DoSomething ==
    /\ guard1                        \* Preconditions
    /\ guard2
    /\ x' = newValue1                \* State changes
    /\ y' = newValue2
    /\ UNCHANGED otherVars
```

### Helper Operators

Extract common logic into named operators:

```tla theme={null}
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

```tla theme={null}
\* Set: processes waiting (order irrelevant)
waiting \subseteq Procs

\* Sequence: message queue (order matters)
queue \in Seq(Messages)
```

## What to Read Next

**Domain-specific examples:**

* [AD Tier Model Specification](/formal-methods/tla-specification) — security invariants for Active Directory
* [Aviation Systems](/formal-methods/aviation-formal-methods-part1) — modeling aircraft operations

**Tools:**

* [MacTLA](/formal-methods/mactla) — native macOS verification with TLC and TLAPS, I wrote it

**External resources:**

* [Learn TLA+](https://learntla.com) — excellent tutorial by Hillel Wayne
* [TLA+ Video Course](https://lamport.azurewebsites.net/video/videos.html) — Leslie Lamport's lectures
* [Specifying Systems](https://lamport.azurewebsites.net/tla/book.html) — the complete TLA+ book