Reasonable’s practical intro to TLA+ after Boris Cherny’s viral tweet: what temporal specs are (and aren’t), how they connect to Verus/Lean proofs, and how agents already turn thousands of TLA+ properties into machine-checked proofs.
The internet discovers TLA+. Now what?
By Anna Mészáros, Szilvia Ujváry, Kseniia Strelbytska, Balázs Szilágyi, and Ferenc Huszár — Reasonable, 25 September 2026
Boris Cherny’s viral TLA+ tweet showed how useful formal models can be in agentic coding. This post gives a practical introduction to what TLA+ is. But TLA+ is only the starting point. We also look at how temporal specifications, modern proof systems and AI agents can fit together, from modeling system behaviour to generating machine-checked proofs, and ultimately toward software that is specified, implemented and verified in one loop.
Boris tweeteth, the internet copy-pasteth
This 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.
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.
What TLA+ is
Our running example is leader election among three computers, a, b and c. Databases rely on leader election being correct. We require that no two leaders exist at the same time.
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 (snapshots) and actions (single steps that change a state).
Temporal properties: 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. Temporal properties are 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 (□ never two leaders). Liveness: something good eventually happens (◇ someone is leader). Liveness requires fairness assumptions (weak fairness WF(A), strong fairness SF(A)).
TLC, the standard TLA+ model checker, enumerates reachable states for a finite instance. A proof makes the stronger statement that the property holds in general.
What TLA+ is not
TLA+ is widely deployed (AWS, MongoDB, Datadog, Kafka), but three caveats matter:
Model checking only goes so far. TLC explores finite instances; proofs are needed for arbitrary sizes.
The model is not the implementation. Spec and code can drift.
TLA+ cannot express every property. Linear temporal logic speaks about individual executions; CTL/ATL can express branching-time and strategic properties.
From TLA+ to proofs
One route is to take the model into a modern proof system:
Lean is interactive and very general.
Verus is auto-active and designed around Rust; specs and proofs can live alongside the real implementation.
Veil is a Lean-based tool for state-machine models.
Why Verus? Closing the spec-to-implementation gap by proving that the implementation refines the model (as Anvil demonstrated). Safety proofs are usually inductive; liveness proofs establish progress under fairness. Much of this work is repetitive — a natural target for proof-generating agents.
From proofs to machine-checked software
Connecting TLA+ models to modern proof systems and implementations opens:
Refinement proofs
Program synthesis from models with proofs
Protocol search with formal correctness as the objective
Richer logics beyond linear time for multi-agent systems
A sneak peek at Reasonable’s progress
A TLA+ to Verus transpiler (algorithmic vs agentic)
A prover–reviewer loop with anti-cheat checks
A dataset: from 16,459 real-world TLA+ spec/property pairs to 3,000+ machine-checked safety and liveness proofs, plus a 40-task evaluation set
An evaluation of closed and open-weight frontier models on temporal proofs