arXiv:2611.02849v1 Announce Type: new
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.
arxiv
TLAPS-Bench: Benchmark for AI-Driven Formal Verification of Real-World Systems
TLAPS-Bench is a new benchmark and execution harness for using AI agents to construct machine-checked proofs of real-world system specifications in TLA+. It includes 265 proof targets from 95 specifications covering cache coherence, Byzantine consensus, and write-ahead logs. Frontier models like GPT-6.1 Sol proved 44.3% of a subset of 70 targets, revealing both progress and remaining challenges in end-to-end proof development.
Provides a concrete, reproducible benchmark for measuring AI capabilities in formal verification of complex systems, a key area for AI safety and reliability.
Comments & Questions (0)
No comments yet
Be the first to comment!