What is TLA+?

It's Not a Programming Language

The biggest mistake beginners make is thinking TLA+ is a programming language. You don't write TLA+ to build an application. You write TLA+ to design a blueprint of how a system behaves — before you write a single line of implementation code.

TLA+ (Temporal Logic of Actions) is a mathematical language for specifying the behavior of concurrent and distributed systems. It was created by Leslie Lamport, the same computer scientist who invented the Paxos consensus algorithm and the concept of logical clocks. He received the Turing Award in 2013 partly for this work.

Thinking in States

When you write code, you think about doing: "First do A, then do B, if C then do D."

When you write TLA+, you think about states and transitions between states.

A state is a snapshot of your entire system at one frozen moment in time — the values of every relevant variable. For example:

account_balance = 100
transfer_in_progress = false
lock_held_by = "nobody"

An action is a transition that moves the system from one state to another. For example, a "StartTransfer" action might change transfer_in_progress to true and set lock_held_by to the requesting process.

The "Specification"

A TLA+ specification is a set of mathematical formulas that describes:

1. The Initial State (Init): The exact values of all variables when the system starts.
2. The Next-State Relation (Next): All possible valid transitions the system can take from any given state. This is a disjunction (OR) of all possible actions.
3. Invariants: Properties that must hold in every reachable state (e.g., "the account balance is never negative").
4. Liveness Properties: Properties about things that must eventually happen (e.g., "every submitted request is eventually processed").

If you can describe your system this way, you can use mathematical tools to explore every possible future state of that system — exhaustively and automatically.