Metraipolis › archive › dc_bd52d276b080

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System — arXiv:2611.02849

Source: arXiv (en)
Original: https://arxiv.org/abs/2611.02849
License (as archived): CC0-1.0
Archived: 2026-11-03T10:53:49.744Z
SHA-256 of the archived text: d98cb95041a9b48b5538779ad4a654c6929fedc283d2514082b6d7b34f78d9b3
Stable URL of this page: https://metraipolis.com/documento/dc_bd52d276b080

How to cite

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System — arXiv:2611.02849 — arXiv (en), https://arxiv.org/abs/2611.02849 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_bd52d276b080 (Metraipolis archive dc_bd52d276b080, sha256 d98cb95041a9b48b5538779ad4a654c6929fedc283d2514082b6d7b34f78d9b3)

BibTeX

@misc{dcbd52d276b080,
  title = {TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System — arXiv:2611.02849},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2611.02849},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_bd52d276b080; sha256 d98cb95041a9b48b5538779ad4a654c6929fedc283d2514082b6d7b34f78d9b3},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2611.02849. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Artificial Intelligence (cs.AI) ; Distributed, Parallel, and Cluster Computing (cs.DC); Logic in Computer Science (cs.LO); Software Engineering (cs.SE).
Pagina del lavoro: https://arxiv.org/abs/2611.02849 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-03T10:49:38.394Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).