Boris Cherny's viral TLA+ tweet, and what TLA+ actually does

This week Boris Cherny used Opus 5.5 to model parts of the Claude Agent SDK in TLA+ and Lean, the post drew about a million views and thousands of bookmarks, while much of the thread asked one question, what TLA+ actually is. The toolkit is over 30 years old, and it keeps appearing in practice: Datadog recently wrote about harness-first agents, and formal models are standard at AWS, MongoDB, Datadog and Kafka.

What TLA+ is

TLA+ (Temporal Logic of Actions) is a language for writing down two things: a transition system, meaning what the system can do, and temporal properties, meaning what must hold in every run. States are snapshots (who is a candidate, who voted for whom, who is the leader), and actions are single steps between them.

The classic example is leader election: three computers, a, b and c, must agree on one leader, and two leaders must never coexist. Safety properties state that nothing bad ever happens; liveness properties state that something good eventually does, for example that a leader is eventually elected. In TLA+ they are written with three simple operators: always, eventually and leads-to.

TLC, the standard model checker, explores every reachable state of a finite model and returns a counterexample whenever a property fails. For three computers the whole space is 38 states; for nine it grows past a million.

What TLA+ is not

Three caveats matter. Model checking only covers finite instances, so a general claim needs a proof, and TLA+'s own prover, TLAPS, has limited automation, especially for liveness. A specification is a separate model of the software: nothing guarantees that the implementation behaves exactly like it, and the two can drift apart as the code changes. And because TLA+ is based on linear temporal logic, properties about alternative futures or strategies, which CTL and ATL can express, remain out of reach.

From models to machine-checked proofs

Modern proof systems go further. Lean is interactive and general, and it was the prover in Boris Cherny's post; Verus is designed around Rust, so specifications and proofs can live beside the real implementation; Veil targets state-machine models and was recently used to verify a sync engine, fixing 17 bugs in the process.

The team at Reasonable is automating part of this path. Their pipeline turned 16,459 real-world TLA+ specification and property pairs into more than 3,000 machine-checked Verus proofs: one agent writes a proof, another reviews it, and a gatekeeper checks that neither modified the spec or taken shortcuts such as assume(false). The goal is software that is specified, implemented and verified in one loop.