The internet discovers TLA+. Now what?
6 hours ago
- TLA+ is a formal modeling language for describing system behaviors and temporal properties, recently popularized in agentic coding via Boris Cherny's tweet.
- It models transition systems with states and actions, and temporal properties like safety (nothing bad happens) and liveness (something good eventually happens).
- TLA+ model checking (TLC) explores finite state spaces; it cannot verify arbitrary system sizes or ensure the implementation matches the model.
- Limitations include the spec-to-implementation gap, limited automation in TLA+'s prover, and the inability to express branching-time or strategic properties beyond LTL.
- Modern proof systems like Lean and Verus can extend TLA+ models toward machine-checked proofs; Verus embeds specifications and proofs with Rust code.
- Reasonable built a pipeline translating 16,459 TLA+ specification/property pairs into over 3,000 machine-checked Verus proofs, using a prover–reviewer loop with anti-cheat checks.
- The work aims to close the gap between formal models and real software through refinement proofs, program synthesis, protocol search, and richer logics for multi-agent systems.
- Future posts will detail the pipeline, dataset, and evaluation of AI models on temporal proof generation.