Boris Cherny recently showcased TLA+, a formal modeling toolkit over 30 years old, by modeling parts of the Claude Agent SDK. The post garnered over 1 million views and thousands of bookmarks, sparking curiosity about the technology. TLA+ provides a compact language for defining what a system is allowed to do and what properties must always or eventually be true.

While TLA+ checks a model of software rather than the implementation itself, and its model checker explores finite instances, modern proof systems can extend its reach. In Verus, specification, proof, and Rust implementation can coexist, and AI can automate much of this process. Reasonable built an agentic pipeline that converted over 16,000 TLA+ specification and property pairs into 3,000+ machine-checked Verus proofs.

The core example involves three computers, a, b, and c, agreeing on a single leader. Databases rely on correct leader election, requiring that no two leaders exist simultaneously. The interactive playground guides users through five levels of the game to learn TLA+ basics.

TLA+ describes transition systems with states and actions, and temporal properties over executions. Safety properties, such as.