AI proving classic distributed-systems protocols in TLA+

Tianyin Xu@tianyin_xu

Thanks for the shoutout to TLA+ @bcherny !

As suggested by Markus Kuppe, let me showcase the brilliant work done by colleagues at Specula and the TLA+ community. While Specula (t.co/hoV6UJIybf) can effectively model system code in TLA+ (and then use model checkers to find hundreds of deep bugs), we can further prove the correctness of system specs using TLAPS. The TLAPS-Bench (t.co/hrYHc4DSow) project aims to offer a proof service for any TLA+ spec of important systems/protocols. Basically, Specula writes the spec; TLAS-Bench generates the proof.

AI writes amazing proofs! We had to retire all Proof-Completion tasks in TLAPS-Bench as they're too easy for frontier AI. We also proved classic protocols and algorithms like 2PC, Paxos, TCP, etc.

However, proving low-level specs of real-world system code _from scratch_ is still non-trivial. @qiancheng9788 ran a subset of TLAPS-Bench using Claude Code w/ Opus 5. The success rate is merely 51.4%. @Muse is great, but Muse Spark 1.3 can only achieve 16.7%.

Ruize has a bag of tricks to push AI agents. Once he pushed Codex to prove one of the nine invariants for the ZooKeeper implementation. Codex struggled 5 days, burned $2000, and did it correctly. We ran out of money to continue. And, @xu_dong_sun shows us that liveness proofs are still difficult for AI without guidance. We have an exciting avenue, but still a lot of work to be done.

If anyone wants to verify their protocols/systems, send us some tokens -- we can do it in TLAPS-Bench. @HacksonClark tells me that people are excited about long-horizon tasks -- TLAPS-Bench may be a perfect benchmark for that.

@bcherny Consider further tuning Claude for TLA+, you may find more bugs and/or prove the correctness of SDK code more efficiently.