Best agent proves 44.3% of targets on a TLA+ system-proof benchmark
TLAPS-Bench gives AI agents a harness for writing machine-checked correctness proofs of system designs in TLA+, a language for specifying how systems behave. It holds 265 proof targets from 95 real-world specifications, including cache coherence, Byzantine consensus and write-ahead logs. Testing Codex with GPT models on 70 targets across 12 specifications, the top model, GPT-6.1 Sol (max), proved 31, or 44.3%. Agents also proved properties of important specifications that were never proved before.