By Anna Mészáros, Szilvia Ujváry, Kseniia Strelbytska, Balázs Szilágyi, and Ferenc Huszár — Reasonable, 25 September 2026
\nBoris 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.
\nThis 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.
\nHere is the short version:
\nOur 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.
\nTLA+ (Temporal Logic of Actions) is a language for writing down two kinds of objects:
\nA TLA+ model declares legal system states and allowed transitions. Temporal properties are built from operators over executions:
\nTwo 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)).
\nTLC, the standard TLA+ model checker, enumerates reachable states for a finite instance. A proof makes the stronger statement that the property holds in general.
\nTLA+ is widely deployed (AWS, MongoDB, Datadog, Kafka), but three caveats matter:
\nOne route is to take the model into a modern proof system:
\nWhy 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.
\nConnecting TLA+ models to modern proof systems and implementations opens:
\nSource: reasonable.io/blog/tla-tutorial
","headings":[{"level":1,"text":"The internet discovers TLA+. Now what?","id":"the-internet-discovers-tla-now-what"},{"level":2,"text":"Boris tweeteth, the internet copy-pasteth","id":"boris-tweeteth-the-internet-copy-pasteth"},{"level":2,"text":"What TLA+ is","id":"what-tla-is"},{"level":2,"text":"What TLA+ is not","id":"what-tla-is-not"},{"level":2,"text":"From TLA+ to proofs","id":"from-tla-to-proofs"},{"level":2,"text":"From proofs to machine-checked software","id":"from-proofs-to-machine-checked-software"},{"level":2,"text":"A sneak peek at Reasonable’s progress","id":"a-sneak-peek-at-reasonable-s-progress"}]}}