Imagine you're a building inspector. You can read blueprints (specifications) and you can walk through a finished house (the implementation), but until now those were two separate jobs — and nobody systematically checked that the house actually matched the blueprints. TLA+, a 30-year-old formal modeling language, is the blueprint. Verus, a Rust-embedded proof system, is the inspector who can read both. This post from Reasonable describes the bridge they're building between the two, and why AI agents are the ones laying the bricks. The viral moment came from Boris Cherny using Opus 5.5 to model parts of the Claude Agent SDK in TLA+ and Lean. ~1M views, thousands of bookmarks. But the Reasonable team's actual contribution sits underneath: they built an agentic pipeline that took 16,000+ TLA+ specification/property pairs and produced 3,000+ machine-checked Verus proofs. That's roughly an 18-19% conversion rate — not spectacular, but enough to demonstrate that the repetitive structure of safety and liveness proofs makes them tractable targets for AI automation. TLA+ itself describes possible system behaviors using temporal logic — states, transitions, and properties like 'no two leaders ever exist simultaneously' (safety) or 'a leader is eventually elected' (liveness). The standard model checker, TLC, enumerates all reachable states for a finite instance. Three computers yield 38 states; nine computers exceed a million. This is the fundamental limitation: model checking is exhaustive but bounded. For general guarantees, you need proofs, and TLA+'s own prover TLAPS has limited automation, especially for liveness arguments that require fairness reasoning (WF1, WF2, SF1, SF2 rules). The key architectural choice is Verus over Lean. Lean is general-purpose and interactive — you write proof steps manually (or have an AI do it). Verus is auto-active and Rust-native: you provide specs and proof structure, an SMT solver handles lower-level reasoning, and critically, specification and proof live alongside the actual implementation. This is what closes the spec-to-implementation gap that has haunted formal methods for decades. Systems like Anvil have demonstrated this manually; Reasonable is automating it. The post also nods to Veil, a Lean-based tool for state-machine verification that recently found 17 bugs in a sync engine, but notes it keeps model and implementation separate. The honest limitations are stated clearly. TLA+ checks a model, not the software itself. The model and code can drift. TLA+ is based on linear temporal logic, which reasons about individual execution traces but cannot express branching-time properties (CTL: 'from any state, a new election can still be started') or strategic properties (ATL: 'this computer has a strategy to become leader regardless of others'). These richer logics matter increasingly for multi-agent systems — exactly the context that triggered the viral interest. What's genuinely novel here is the pipeline concept: TLA+ spec → temporal property → Verus proof → Rust implementation, with AI agents automating the middle steps. The 3,000+ proofs demonstrate feasibility at scale. The successor questions are obvious: Can this pipeline handle liveness proofs at the same rate as safety proofs? Can refinement proofs — proving the Rust implementation actually follows the TLA+ model — be automated? Can the pipeline synthesize implementations from specs, not just verify existing ones? The post hints at all three directions but delivers numbers only on the first. The field fight this participates in is real: formal methods have been 'ten years away from practical adoption' for forty years. The bet here is that LLMs change the economics. If the bottleneck was always the labor cost of writing proofs, and agents can generate proofs at 18%+ conversion rates today with improvement curves ahead, then the adoption barrier drops dramatically. The post positions Reasonable as training models specifically for this — not general-purpose coding agents, but agents that move fluently between specifications, proofs, and implementations.
