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.
Why it matters: Provides a concrete, reproducible benchmark for measuring AI capabilities in formal verification of complex systems, a key area for AI safety and reliability.