The internet discovers TLA+. Now what?

A recent viral example of applying TLA+ to agentic coding sparked broad interest in what TLA+ actually does and how it fits into verification workflows. TLA+ (Temporal Logic of Actions) describes systems as state-transition systems plus temporal properties over executions: safety properties that "nothing bad ever happens" and liveness properties that "something good eventually happens." The standard model checker TLC exhaustively explores finite instances and returns counterexamples for safety violations, but proving properties for arbitrary sizes requires proofs and fairness assumptions for liveness. Crucially, a TLA+ model reasons about possible behaviors, not an implementation, so correctness of the model does not automatically guarantee the running software behaves the same way.

To bridge that gap, modern proof systems and automation are brought into play. Interactive provers like Lean, auto-active systems like Verus (designed around Rust), and tools such as Veil offer routes to machine-checked proofs and tighter links to implementations; Verus enables proving that Rust code refines a TLA+ model. Automation targets repetitive proof work - inductive safety proofs, progress arguments for liveness - and makes proof generation a natural application for agents. Work described includes a TLA+→Verus transpiler and an agentic pipeline that transformed 16,000+ TLA+ spec/property pairs into 3,000+ machine-checked Verus proofs, pointing toward refinement proofs, program synthesis from specs, protocol search, and extensions beyond linear-time logics.