AI helps prove real systems are mathematically correct
TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System
Artificial IntelligenceDistributed, Parallel, and Cluster ComputingLogic in Computer ScienceSoftware Engineering
Summary
Proving complex computer systems work correctly is very hard and needs detailed reasoning. The authors created TLAPS-Bench, a set of challenges and tools that let AI programs help write these proofs in the TLA+ language. They tested AI models on real system problems and showed that the best AI could complete almost half of the proof goals. This work highlights both how useful AI can be and the difficulties that remain in automated proof writing.
What this means in practice
- •For software engineers: Build machine-checked proofs of complex system behaviors using AI-assisted tooling on existing TLA+ specifications.
- •For database operators: Confirm correctness properties of write-ahead log systems using AI-supported formal proofs to reduce bugs.
Authors
Qian Cheng, Ruize Tang, Saad Mohammad Rafid Pial, Zhizhen Cathy Cai, Yiming Su, Jackson Clark, Munim Thahmid, Mahdiya Rahman Sukanya, Chris Newcombe, Igor Konnov, Stephan Merz, Xudong Sun, Murat Demirbas, Yu Huang, Markus Alexander Kuppe, Tianyin Xu
Abstract
TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI. Proving correctness of complex system specifications requires discovering inductive invariants, reasoning about intricate state transitions, and decomposing proofs into tractable obligations. TLAPS-Bench provides a proof harness that supports iterative proof development atop the TLA+ Proof System (TLAPS), where agents are equipped with proof tools and libraries, with safeguards against reward hacking. Using the harness, we have employed AI agents to prove desired properties for important system specifications that were not proved before, spanning cache coherence, Byzantine consensus, and write-ahead logs. TLAPS-Bench contains 265 proof targets (each encodes a property to prove) from 95 TLA+ specifications of real-world systems. We evaluated frontier AI agents, represented by Codex with GPT models, on a subset of 70 proof targets across 12 specifications. The highest-scoring model, GPT-6.1 Sol (max), proved 31 (44.3%) proof targets. The results show challenges and opportunities in end-to-end proof development.