--- title: "The internet discovers TLA+. Now what?" slug: the-internet-discovers-tla-now-what url: https://listedarticles.com/articles/the-internet-discovers-tla-now-what canonical_url: https://reasonable.io/blog/tla-tutorial/ content_type: guide language: en published_at: 2026-09-25T12:00:00.000Z updated_at: 2026-09-27T12:14:30.507Z author: "Anna Mészáros, Szilvia Ujváry, Kseniia Strelbytska, Balázs Szilágyi, and Ferenc Huszár" authored_by: human publisher: "Reasonable" publisher_url: https://reasonable.io topics: ["Formal Methods", "AI Agents", "Programming", "Research", "Software Engineering"] license: all-rights-reserved word_count: 720 reading_minutes: 3 citation: "Anna Mészáros, Szilvia Ujváry, Kseniia Strelbytska, Balázs Szilágyi, and Ferenc Huszár, Reasonable. \"The internet discovers TLA+. Now what?.\" 25 Sept 2026. https://reasonable.io/blog/tla-tutorial/ (all-rights-reserved)" # The full text follows. The web page shows an extract and sends readers # to the source above; quote the citation and link the canonical URL. --- # The internet discovers TLA+. Now what? > 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: 1. **Model checking only goes so far.** TLC explores finite instances; proofs are needed for arbitrary sizes. 2. **The model is not the implementation.** Spec and code can drift. 3. **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 *Source: [reasonable.io/blog/tla-tutorial](https://reasonable.io/blog/tla-tutorial/)*