Pangram verdict · v3.3
We believe that this text is a mix of AI and human-written content.
AI likelihood · overall
MixedArticle text · 1,191 words · 9 segments analyzed
Boris tweeteth, the internet copy-pastethThis week Boris Cherny graced TLA+, a formal modeling toolkit that is over 30 years old, with a tweet. He used Opus 5.5 to model parts of the Claude Agent SDK in TLA+ and Lean, and the internet did what it does: ~1M views, thousands of bookmarks, and people are asking what TLA+ actually is. Boris's post is a great showcase, and it adds to early examples showing that TLA+ is well worth the effort in agentic coding: see Datadog's post on harness-first agents.If you are one of the people now wondering what TLA+ is and what it is for, you are in the right place. TLA+ happens to be one of the formal techniques our team has dived deep into.But there is also a larger reason we care about it.
TLA+ gives us a compact language for saying what a system is allowed to do and what must always or eventually be true of it. That is a useful starting point for verification, but it is not the end of the story.Here is the short version:TLA+ describes possible system behaviours and the properties those behaviours should satisfy.TLA+ itself does not fully verify an implementation. It checks a model of the software, not the software itself, and its main model checker only explores finite instances.Modern proof systems can take us further.
In Verus, specification, proof and Rust implementation can live in the same language.AI can already automate part of this process. We built an agentic pipeline that turned 16,000+ TLA+ specification/property pairs into 3,000+ machine-checked Verus proofs.The interesting question, then, is not only whether an agent can write TLA+. It is what becomes possible once agents can move between specifications, proofs and real programs.Part of our work at Reasonable is training models to enable agents to do this, consistently, reliably, quickly.What TLA+ isOur running example is the one in the interactive playground below, where three computers, a, b and c, have to agree on which of them is the leader. Databases rely on leader election being correct. We require that no two leaders exist at the same time. You can click through the playground to learn the basics of TLA+ through the five levels of the game.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 fashionableWhat TLA+ is notTLA+ is increasingly widely deployed because this way of reasoning about systems can be practically useful; you'll see it in use at AWS, MongoDB, and Datadog, in Kafka, and many other places.
But there are three important caveats, where TLA+ alone stops short of full software verification.Model checking only goes so far. In practice, people most often use TLA+ with TLC. TLC explores every possible run, but only for a finite model. In our example, the state space grows from 38 states with three computers to more than a million with nine. To establish a property for arbitrary system sizes, you need a proof. TLA+'s own prover, TLAPS, can do this in some cases, but its automation is limited, particularly for liveness arguments.The model is not the implementation. A TLA+ specification is usually a separate model of the software. Nothing automatically guarantees that the implementation behaves exactly like the model, and the two can drift apart as the code changes. This is one element of the classic spec-to-implementation gap.TLA+ cannot express every property we may want. TLA+ is based on linear temporal logic, which makes statements about individual executions: "In every run, a leader is eventually elected." But some interesting properties concern alternative futures or strategies.CTL, a branching-time logic, can express statements such as: "from any state, a new election can still be started."ATL can express strategic statements such as: "this computer has a strategy to become a leader whatever the others do."These richer properties become relevant once we start thinking about systems containing multiple competing or collaborating agents.So TLA+ gives us an unusually useful language for describing temporal behaviour, but a complete verification stack needs more: stronger proof machinery, a connection to real code, and eventually richer logics.From TLA+ to proofsOne route is to take the model into a modern proof system.
There are several options, examples include:Lean is interactive: you (or an AI) write the proof step by step. It is very general, widely used in mathematics, and was the prover used in Boris's post.Verus is auto-active and designed around Rust.