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.
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.
Part of our work at Reasonable is training models to enable agents to do this, consistently, reliably, quickly.
Our running example is the one in the interactive playground below, where three computers, a, b and c, have to agree on which of them is the leader. Databases rely on leader election being correct. We require that no two leaders exist at the same time. You can click through the playground to learn the basics of TLA+ through the five levels of the game.
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, which are snapshots of the system (who is a candidate, who has voted for whom, who is leader) and actions, single steps that change a state ("a starts an election", "b votes for a"). In the interactive playground, you take these steps by hand, exploring one possible run the way a tester would.
Temporal properties are 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 between these states. For example, in the election, any of a, b or c may start an election from the initial state, voting for itself as it does so, and b may vote for a or for c.
□ 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.
TLA+ is increasingly widely deployed because this way of reasoning about systems can be practically useful; you'll see it in use at AWS, MongoDB, and Datadog, in Kafka, and many other places. But there are three important caveats, where TLA+ alone stops short of full software verification.
CTL, a branching-time logic, can express statements such as: "from any state, a new election can still be started."
ATL can express strategic statements such as: "this computer has a strategy to become a leader whatever the others do."
These richer properties become relevant once we start thinking about systems containing multiple competing or collaborating agents.
One route is to take the model into a modern proof system. There are several options, examples include:
Lean is interactive: you (or an AI) write the proof step by step. It is very general, widely used in mathematics, and was the prover used in Boris's post.
Verus is auto-active and designed around Rust. You provide specifications and the important proof structure, while an automated solver handles much of the lower-level reasoning.
Veil is a Lean-based tool built specifically for state-machine models. Leo de Moura has recommended it, and it was recently used to verify a sync engine, fixing 17 bugs in the process. Liveness remains future work, however, and the verified model is still separate from the implementation.
Why use Verus? Because specifications and proofs can live alongside the real Rust implementation. That matters because it gives us a route towards closing the spec-to-implementation gap: instead of proving properties only about a separate abstract model, we can ultimately prove that the implementation refines that model. Systems such as Anvil have already demonstrated this style of verification; our work at Reasonable builds particularly closely on Anvil.
Safety proofs are usually inductive. Show that the property holds initially, then show that every possible action preserves it. Much of the work consists of splitting over the different actions and tracking the relevant invariants.
Liveness proofs establish progress. Typically, some quantity decreases as the system progresses, together with fairness assumptions ruling out executions in which an enabled action is postponed forever. Rules such as WF1, WF2, SF1 and SF2 package these arguments; our temporal library implements them as proven Verus lemmas.
A large fraction of this work is repetitive: tracking invariants, splitting over actions, supplying intermediate lemmas and filling in solver-visible details. That makes it a natural target for proof-generating agents.
Automated theorem proving has recently made rapid progress in mathematics. Software verification poses a somewhat different problem: before proving anything, we need a useful description of what the software is supposed to do.
Refinement proofs. Prove that the Rust implementation follows the TLA+ model. Anvil demonstrated this manually. Automating more of that process would reduce the gap between verifying a model and verifying the software that implements it.
Program synthesis. Start from the model and generate an implementation together with a proof that the implementation refines it. In this setting, the formal specification constrains both code generation and verification.
Protocol search. Once checking a candidate protocol is cheap enough, the verifier can become an objective function: generate variants of a protocol, verify them, and retain those satisfying the desired properties. This starts to look similar to systems such as AlphaEvolve, except that correctness is checked formally rather than estimated by tests.
Beyond linear time. Some properties of multi-agent systems concern alternative futures or strategies rather than individual execution traces. Expressing those requires logics beyond LTL. Benjamin Brast-McKie's work explores this side of the problem, while our current work focuses on proving temporal properties and connecting them to programs.
We have been working on a pipeline for translating TLA+ specifications into machine-checked Verus proofs. Our next blog posts will describe the individual pieces in more detail. For now, the main results are:
A TLA+ to Verus transpiler. We built an algorithmic transpiler and compared it with an agentic alternative in which an LLM produces the translation and a second LLM reviews it.
A prover–reviewer loop with anti-cheat checks. One agent writes a proof and another reviews it. A separate gatekeeper checks that the agents have not modified the specification or introduced shortcuts such as assume(false).
A dataset of temporal proofs in Verus. Starting from 16,459 real-world TLA+ specification/property pairs, the pipeline produced more than 3,000 machine-checked safety and liveness proofs. We also constructed a 40-task evaluation set.
An evaluation of current models. We tested both closed and open-weight frontier models on the evaluation set, looking at which temporal proofs they can complete and where the remaining failure modes are.
We'll cover those results in the follow-up posts.
We're hiring people excited to push the boundaries of formal verification and AI agents. If you want to help build systems where correctness can be machine-checked, we'd love to hear from you: Careers.