Claude Opus 5.5 models the Agent SDK in TLA+, and formal methods trend

This week, Boris Cherny posted the results of asking Claude's Opus 5.5 to model parts of the Claude Agent SDK in TLA+ and Lean. According to Reasonable, whose follow-up post on the moment reached Hacker News' front page, the tweet pulled in roughly a million views and thousands of bookmarks, and left a large audience asking a basic question: what is TLA+?

What TLA+ is

TLA+, short for Temporal Logic of Actions, is a formal modeling language that has existed for more than three decades. As Reasonable explains, a TLA+ model describes two things: a transition system, meaning the states a system can occupy and the single steps that move between them, and temporal properties, which are claims about how an execution unfolds over time.

Reasonable's running example is a leader election among three computers, with the requirement that two leaders never exist simultaneously. TLA+ deliberately imposes no ordering on transitions and does not model how probable different events are, which Reasonable calls the right abstraction for distributed systems, where messages, timeouts and user actions can interleave in many orders.

Properties come in two flavours. Safety says nothing bad ever happens; liveness says something good eventually does. Reasonable points out that a system which sits idle forever is perfectly safe, which is why liveness also matters, and why it needs fairness assumptions, such as requiring that an action which stays enabled must eventually be taken.

The standard model checker, TLC, verifies these properties by enumerating every reachable state of a finite instance. For three computers that means 38 states, and the checker confirms no two leaders coexist. Change one rule so a computer can vote twice, and TLC returns a six-step counterexample ending with two leaders. At nine computers the state space exceeds a million states, which previews the tool's central limitation.

Three places TLA+ runs out

Reasonable is blunt that a TLA+ model is not the same as full software verification, and lists three gaps.

First, model checking only covers finite instances. Establishing a property for arbitrary system sizes requires a proof, and TLA+'s own prover, TLAPS, has limited automation, particularly for liveness arguments.

Second, the model is not the implementation. Nothing automatically guarantees that the code behaves like the specification, and the two can drift apart as the code changes, the classic spec-to-implementation gap.

Third, expressiveness. TLA+ rests on linear temporal logic, which makes claims about individual executions. Branching-time logics such as CTL can state that a fresh election can still be started from any state, and strategic logics such as ATL can state that one computer has a strategy to become leader regardless of what the others do, the kind of property that grows relevant when a system contains multiple interacting agents.

None of this has blocked adoption. Reasonable notes that TLA+ is in use at AWS, MongoDB and Datadog, and inside Kafka, and that Datadog has published on harness-first agents as an early sign that TLA+ pays off in agentic coding. Jack Vanlightly has also been teaching TLA+ on his blog since long before agents made it fashionable.

From specifications to proofs and code

The route past those limits runs through modern proof systems, of which Reasonable highlights three. Lean, the prover used in Cherny's post, is interactive and general purpose. Verus is built around Rust, so specifications, proofs and the real implementation live in a single language, a direct attack on the spec-to-implementation gap. Veil, a Lean-based tool for state-machine models that Leo de Moura has recommended, was recently used to verify a sync engine and fixed 17 bugs in the process, though liveness remains future work and the verified model is still separate from the implementation.

AI is already moving into this pipeline. Reasonable says it built an agentic pipeline that converted more than 16,000 TLA+ specification and property pairs into over 3,000 machine-checked Verus proofs, evidence that part of the path from model to proof can now be automated.

Why it matters

The viral tweet is a symptom, not the story. Agent-written specifications only matter if something checks them, and the question Reasonable poses is not whether an agent can write TLA+ but what becomes possible once agents move fluidly between specifications, proofs and real programs. Formal methods have always stalled on cost: state-space explosion, manual proofs, and models that drift away from the code they describe. If agents can routinely translate specifications into machine-checked proofs tied to the implementation itself, verification stops being a specialist activity reserved for database internals and becomes part of ordinary agent-driven development. For teams building agent harnesses, where subtle ordering and retry bugs are the norm, that shift is likely to arrive first.