Intro to TLA+ for the LLM Era: Prompt Your Way to Victory
Most engineers’ first objection to using TLA+ is, the syntax is hostile. It looks like LaTeX, not like code. But now, frontier LLMs can generate TLA+ easily. It’s still your responsibility to understand your system and define what “correctness” means, and you need a high-level understanding of temporal logic. I’ll explain temporal logic in this article. At the end I’ll show an example prompt to start a TLA+ spec with Claude.
Subscribe for new articles
A toy problem
Here’s a classic puzzle. You have a can of beans. Each bean is white or black. The can starts nonempty. While there are at least 2 beans:
Choose 2 beans.
If they’re the same color: discard both, add 1 white bean.
If they’re different colors: discard both, add 1 black bean.
Two questions:
Can the number of beans ever reach zero?
If the algorithm terminates with b = 1, what must have been true at the start?
You could think really hard. Or you could write it down in TLA+ and let a model checker answer both questions automatically. The whole point is to avoid thinking—or at least, to have a machine verify that your thinking was correct. Or convince your friends that your thinking is correct, or convince the peer-review panel for your research paper.
How logical formulae produce a state machine
TLA+ was invented by Leslie Lamport in the 1990s. TLA stands for “Temporal Logic of Actions,” and TLA+ is the name of the specific language. TLA+ has basic boolean logic, and it has sets and functions, and quantification (“for all” and “there exists”). It also has temporal operators, which we’ll see soon.
When you write a specification in TLA+, you’re writing a logical formula which defines a state machine. The machine has a fixed set of variables, and each state is an assignment of values to the variables. For the can problem, there are variables: w (the number of white beans) and b (the number of black beans). Each state is an assignment of values to w and b. A behavior is a sequence of states, and a specification is the set of allowed behaviors.
Initial state
We need an initial-state rule—a predicate that’s true of exactly the states we’re willing to start from. In English: “the can is initially nonempty,” or w + b > 0. Which of these initial states matches the predicate?
b = 0 /\ w = 0<br>b = 0 /\ w = 4<br>b = 6 /\ w = 1<br>b = 1 /\ w = "foo"
In TLA+ “/\” means “and”, so b = 0 /\ w = 0 means “b = 0 and w = 0”.
The second and third states match the predicate. The first doesn’t, because w and b sum to zero, and the final state doesn’t make sense because you can’t add 1 and the string “foo”. TLA+ has no type system, only sets, so there’s nothing stopping w from being a string. Lamport calls something like that “silly.” We prevent silly states by specifying that w and b must be natural numbers:
EXTENDS Integers<br>Init == w \in Nat /\ b \in Nat /\ w + b > 0
EXTENDS Integers imports everything you need for handling integers, like the set of natural numbers Nat, and \in is the set-membership operator ∈\in. In TLA+, == means “defined as.” This is confusing, because it’s kind of the opposite of C: a single = tests for equality, and == names a formula (like a macro).
State transitions
A state-transition rule is a predicate over two states—current and next—that says which transitions are legal. Let’s turn our algorithm into a state-transition rule in TLA+.
Starting from English:
2 white beans: remove 2 whites, add 1 white → net effect: w -= 1
2 black beans: remove 2 blacks, add 1 white → net effect: b -= 2
1 of each: remove 1 white and 1 black, add 1 black → net effect: w -= 1
Notice the first and third cases have identical effects on the state: both just subtract 1 from w and leave b alone. This is the kind of insight that falls out naturally when you write things down precisely.
In TLA+ these become three actions :
WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b \* Picked 2 white<br>BB == b > 1 /\ b' = b - 2 /\ w' = w + 1 \* Picked 2 black<br>WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* Picked 1 of each
There are two operators that we’re seeing for the first time here. The prime (') operator means “the next value of this variable”: w' = w - 1 means “in the next state, w will equal the current w minus 1.” UNCHANGED b is shorthand for b' = b. You have to account for every variable in every action—TLA+ won’t assume that unmentioned variables stay the same. This is annoying, but it forces you to think about what each action does to the whole state.
The terms without primes are the guard : conditions that must hold now for the action to fire. The terms with primes are the assignment : what the next state looks like. If the guard is...