TLA+ (Temporal Logic of Actions) is a language for writing down two kinds of objects:
A transition system: what the system can do. There are states, which are snapshots of the system (who is a candidate, who has voted for whom, who is leader) and actions, single steps that change a state ("a starts an election", "b votes for a"). In the interactive playground, you take these steps by hand, exploring one possible run the way a tester would.
Temporal properties are statements about how a run plays out over time. For example, "There are never two leaders." "A leader is eventually elected."
A TLA+ model declares legal system states and allowed transitions between these states. For example, in the election, any of a, b or c may start an election from the initial state, voting for itself as it does so, and b may vote for a or for c.
It imposes no order on transitions and does not attempt to model the probability distribution of different events happening, which is the right abstraction for distributed systems, where messages, timeouts and user actions can happen in many different orders.
The underlying mathematics is simple, it uses sets, true/false statements and relations. Temporal properties are then built from operators over executions:
□ P (always P ): P holds in every state visited.
◇ P (eventually P ): P holds in some future state.
P ⇝ Q (P leads to Q): whenever P holds, Q eventually holds afterwards.
Two kinds of property matter particularly often.
Safety: nothing bad ever happens. For our election: □ (there are never two leaders). In the playground, the model checker explores every possible state: all 38 states for three computers, and confirms the property. Level 2 changes one rule so that a computer can vote twice. The checker then returns a six-step execution ending with two leaders. That execution is a counterexample: a concrete way the model can violate the property.
Liveness: something good eventually happens. Safety alone is not enough. A system that does nothing forever is perfectly safe. So we might also require: ◇ (someone is leader). Level 3 shows why this matters: a typo stops anything from happening, and the safety check still passes. Liveness requires fairness assumptions, which rule out executions where an action remains possible forever but is simply never taken. Weak fairness WF(A) says that an action that stays enabled must eventually happen; strong fairness SF(A) covers actions that become enabled infinitely often.
The mental model is simple: a TLA+ model describes the possible execution traces of a system, and a property describes which traces are acceptable. Verification asks whether every possible trace is acceptable.
TLC, the standard TLA+ model checker, answers this by enumerating reachable states for a finite instance. A proof makes the stronger statement that the property holds in general.
For more, Jack Vanlightly has been teaching TLA+ on his blog long before agents made it fashionable