< up >
2026-05-28

TLA+ - cheat sheet

TLA+ is a formal specification language to model and proof systems. You basically model your system as state machine and let the model checker find deadlocks by going through each legal state transition. The language was invented by L. Lamport, also famously known for LaTeX and Lamport clocks.

Unchanged Sets

Variables are set to null after any satisfied action. This default is quite counter-intuitive in contrast to virtually any other programming language. The prime of a variable can be used to set its value for the next action using '. E.g. i' is the prime for the variable i

VARIABLE i

Increment == i' = i + 1
Init == i = 0
Next == Increment

I think of a variable like a math function with step t where “‘” refers to the next t: f(t+1) = f(t) + 1

If the value shouldn’t change, the prime can be set to the original variable: i' = i. This can become quite unreadable having many variables. UNCHANGED can be used to keep a sequence of variables as-is:

VARIABLE tee
VARIABLE coffee

DrinkCoffee ==
  /\ coffee' = coffee + 1
  /\ UNCHANGED <<tee>>

With many variables and many actions that change different variables, those UNCHANGED sequences can also become quite hard to read. For many actions sharing the same unchanged variables, those can be outsourced to a set.

VARIABLE tee
VARIABLE coffee
VARIABLE water
VARIABLE juice

NotWater == <<tee, coffee, juice>>

DrinkWater == 
  /\ water' = water+1
  /\ UNCHANGED NotWater

If there are unchanged variables outside the set, they can be added to the action using another UNCHANGED statement.

HotBeverages == <<tee, coffee>>

DrinkWater ==
  /\ water' = water+1
  /\ UNCHANGED HotBeverages
  /\ UNCHANGED juice

Special Actions

Init and Next are special actions:

Init gets executed at very first and usually initialized variables. It’s the only exception where variables get assigned directly and not it’s prime '.
Next is an action containing atomic actions. If Next can’t be satisfied, the model checker detects a deadlock.

Both actions need to be registered as Init and Next within the model settings. The action names itself are arbitrary, but we’ll stick with Init and Next for simplicity.

Structs

While the actions implement any logic that may reflect an already existing application or prototype, constraints can be used to ensure conditions that should always stay true. This can be quite useful to get logic errors. Otherwise the model checker tries to find a next state and aborts with a deadlock error if not.

Invariants

Actions that must always be satisfied are called invariants. They can be added to the model settings Model Overview -> What to check? -> Invariants.

VARIABLES maintenance_mode
VARIABLES user_logged_in

\* If maintenance-mode is enabled, user shouldn't be logged in anymore
MaintenanceInvariant == (maintenance_mode = TRUE) => (user_logged_in = FALSE)

Since variables are not typed, type checks can also be implemented using invariants:

EXTENDS Naturals \* import the set of natural numbers

VARIABLES id
Init == id = 0
TypeIdInvariant == id \in Nat

Constants

Constants can be set in the model settings for parameterization via Model Overview -> What is the model?. They don’t need to be checked using invariants within any step. It’s enough to check them at the beginning once using ASSUME.

EXTENDS Naturals
CONSTANT id
ASSUME id \in Nat

Impressions

Model Overview of the TLA+ “Toolbox” eclipse application containing essential model settings.