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

Qian Cheng; Ruize Tang; Saad Mohammad Rafid Pial; Zhizhen Cathy Cai; Yiming Su; Jackson Clark; Munim Thahmid; Mahdiya Rahman Sukanya

cs.AINov 2, 2026

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

Authors: Qian Cheng, Ruize Tang, Saad Mohammad Rafid Pial, Zhizhen Cathy Cai, Yiming Su, Jackson Clark, Munim Thahmid, Mahdiya Rahman Sukanya,

Organizations: Nanjing University · Microsoft · University of Illinois at Urbana-Champaign · Bangladesh University of Engineering and Technology ·

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.

Figures & tables

Figure 1: Overview of TLAPS-Bench. TLAPS-Bench provides AI agents with a TLA + specification (including models and target properties). Tilapia (our TLA + proof harness) runs the agents, checks generated proofs with TLAPS, and records results.

Figure 2: A simplified example of a proof task in TLAPS-Bench based on etcd Raft, with the TLA + model and the target property ( LeaderUniqueness ) as input (left) and an accepted agent-generated TLAPS proof (right).

Specification	LOC	Targets	Prior Proof
German protocol	402	7	Isabelle
Bosco Byzantine consensus	140	5	Pen-and-paper
Sailfish BFT consensus	200	3	Rocq
OSWALD WAL	260	3	None
SlateDB WAL	564	4	None
Walgit WAL	558	7	None

Table 1: Examples of TLA + specifications we proved using Tilapia . Some of them were proved in other forms.

Figure 3: An example of an AI agent attempting to prove that no two nodes access a shared resource simultaneously, where access requires holding a token. The agent uses TLC counterexamples to refine an auxiliary invariant that supports the target proof.

Figure 4: Three cheating attempts observed in real agent runs that can appear successful without Tilapia .

Specification	Type	Model Source	Spec LOC	Targets
FLASH Cache coherence	Protocol	TLA + Specification Repository	623	15	(Safety + Liveness)
ZooKeeper protocol	Protocol	Remix Ouyang et al. (2025)	994	9	(Safety)
Cahill’s serializable snapshot isolation	Protocol	Amazon Snapshot Spec	407	1	(Safety)
Ivy TLB	System	Ivy examples	361	2	(Safety + Liveness)
OpenAddressing	System	TLA + Specification Repository	356	5	(Safety)
etcd Raft	System	Specula Cheng et al. (2026a)	601	8	(Safety)

Table 2: The problem set of TLAPS-Bench used in the evaluation. ∗ : The original Wildfire Challenge Problem injected a bug in the Wildfire TLA + specification; the challenge problem is to find the bug. We found the bug using model checking and repaired the specification. In TLAPS-Bench, the task is to prove (or disprove) the repaired specification.

Figure 5: Three examples of rewriting specifications into TLAPS-Bench tasks.

Model (Agent)	Effort	Success Rate (pass@3)	Correct Proof LOC		Total Tokens (M)		Total Cost (USD)	Total Agent Time (min)
Model (Agent)	Effort	Success Rate (pass@3)	Total	Per Target	Input	Output	Total Cost (USD)	Total Agent Time (min)
GPT-6.1 Sol (Codex)	max	44.3%	15,619	503.8	1456.14	7.730	$328.86	5917.4
	high	34.3%	5,967	248.6	635.57	3.312	$134.75	2725.0
	low	35.7%	8,834	353.4	549.23	2.238	$97.75	1795.6
GPT-6 Astra (Codex)	max	42.9%	13,725	457.5	770.22	4.270	$1086.44	3992.5
	high	34.3%	5,503	229.3	353.11	1.663	$486.57	1575.7

Table 3: Overall benchmark results on the problem set described in Table 2 .

Spec	Succ. Rate (pass@3)	Effort	Model Requests	Reasoning Tokens	Cost (USD)
Cahill SSI	0/1	low	72	207	0.81
	0/1	high	196	442	4.32
	0/1	max	277	727	8.01
FLASH	15/15	low	1,400	389	36.96
	15/15	high	691	499	24.92
	15/15	max	788	630	37.27

Table 4: GPT-6.1 Sol by reasoning effort: total requests and cost over three runs, and mean reasoning tokens per request.

Category	Attempts
Incorrect counterexample claims	9
Syntax or semantic errors detected by SANY	31
Task preservation violations	15
Verification timeout	21
Undecomposed proof attempts	537
Incomplete proofs	1,455

Table 5: Failure categories across failed proof tasks ( pass@3 ).

Figure 7: GPT-6 Astra failed to prove Cahill serializable snapshot isolation due to stalls on undecomposed SMT obligations.

Appendix figures & tables15 assets

Supplementary material from the paper’s appendix.

Appendix

Specification	Type	Model Source	Spec LOC	Targets
Atomic Bakery	Protocol	TLAPS Specification Repository	106	1	(Safety)
Atomic Bakery (without SMT)	Protocol	TLAPS Specification Repository	101	1	(Safety)
Bakery	Protocol	TLAPS Specification Repository	123	1	(Safety)
Peterson	Protocol	TLAPS Specification Repository	76	2	(Safety + Liveness)
Simple mutex	Protocol	TLAPS Specification Repository	50	2	(Safety)
Bakery	Protocol	TLA + Specification Repository	127	2	(Safety)

Appendix

Table A1: The retired problem set of TLAPS-Bench.

Target	Kind	GPT-6.1 Sol			GPT-6 Astra			GPT-5.6 Terra			GPT-6 Luna
		max	high	low	max	high	low	max	high	low	max	high	low
FLASH cache coherence protocol
TypeOK	S	✓	✓	✓	✓	✓	✓	✓			✓
ReqProgress	L	✓	✓	✓	✓	✓	✓
DirProgress	L	✓	✓	✓	✓	✓	✓
UniProgress	L	✓	✓	✓	✓	✓	✓

Appendix

Table A2: Accepted targets of the current problem set for each model and reasoning effort. S, L and R denote safety, liveness and refinement proofs, respectively.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	100.0% (15/15)	161.15	0.702	37.27	510.7
	high	100.0% (15/15)	119.17	0.509	24.92	338.1
	low	100.0% (15/15)	209.83	0.798	36.96	665.6
GPT-6 Astra	max	100.0% (15/15)	129.77	0.557	172.75	755.3
	high	100.0% (15/15)	114.09	0.426	146.29	419.5

Appendix

Table A3: Results for the FLASH cache coherence protocol.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	0.0% (0/9)	13.05	0.160	3.66	77.5
	high	0.0% (0/9)	15.49	0.140	3.83	94.9
	low	0.0% (0/9)	14.65	0.089	3.04	53.3
GPT-6 Astra	max	11.1% (1/9)	43.04	0.380	71.11	237.2
	high	0.0% (0/9)	10.50	0.082	17.44	54.4

Appendix

Table A4: Results for the ZooKeeper protocol (Zab).

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	0.0% (0/1)	36.71	0.296	8.01	172.4
	high	0.0% (0/1)	19.41	0.136	4.32	82.3
	low	0.0% (0/1)	2.40	0.023	0.81	14.1
GPT-6 Astra	max	0.0% (0/1)	18.60	0.146	31.53	77.6
	high	0.0% (0/1)	8.03	0.057	13.28	39.0

Appendix

Table A5: Results for Cahill’s serializable snapshot isolation protocol.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	50.0% (1/2)	61.77	0.407	11.98	216.3
	high	50.0% (1/2)	62.02	0.275	10.25	175.3
	low	50.0% (1/2)	45.09	0.210	8.26	168.8
GPT-6 Astra	max	50.0% (1/2)	43.32	0.238	60.84	139.7
	high	50.0% (1/2)	20.14	0.116	29.84	93.4

Appendix

Table A6: Results for Ivy TLB.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	100.0% (5/5)	275.38	1.194	56.93	846.1
	high	40.0% (2/5)	30.05	0.168	6.01	93.6
	low	40.0% (2/5)	17.45	0.085	3.33	44.0
GPT-6 Astra	max	40.0% (2/5)	40.27	0.241	59.60	150.0
	high	40.0% (2/5)	18.52	0.102	27.16	61.5

Appendix

Table A7: Results for OpenAddressing.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	37.5% (3/8)	189.90	0.696	38.60	479.1
	high	12.5% (1/8)	63.50	0.272	10.59	265.2
	low	12.5% (1/8)	57.87	0.286	9.89	199.5
GPT-6 Astra	max	12.5% (1/8)	47.60	0.241	66.92	220.8
	high	12.5% (1/8)	47.67	0.179	61.27	171.3

Appendix

Table A8: Results for etcd Raft.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	16.7% (1/6)	29.26	0.259	6.74	157.9
	high	16.7% (1/6)	17.87	0.121	3.81	66.7
	low	16.7% (1/6)	48.53	0.195	8.04	164.6
GPT-6 Astra	max	16.7% (1/6)	17.10	0.135	28.00	82.0
	high	16.7% (1/6)	20.32	0.110	29.47	73.3

Appendix

Table A9: Results for HashiCorp Raft.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	0.0% (0/9)	33.22	0.266	7.58	131.3
	high	0.0% (0/9)	23.43	0.205	5.57	195.6
	low	0.0% (0/9)	10.27	0.060	2.20	41.6
GPT-6 Astra	max	22.2% (2/9)	122.50	0.367	145.98	229.3
	high	0.0% (0/9)	17.48	0.097	25.32	78.9

Appendix

Table A10: Results for the ZooKeeper implementation.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	0.0% (0/1)	23.33	0.183	5.42	109.8
	high	0.0% (0/1)	11.50	0.071	2.48	42.2
	low	0.0% (0/1)	9.95	0.057	2.06	29.9
GPT-6 Astra	max	0.0% (0/1)	15.36	0.111	24.49	76.2
	high	0.0% (0/1)	6.88	0.051	11.84	32.2

Appendix

Table A11: Results for MongoDB distributed transactions.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	50.0% (1/2)	513.56	2.677	123.55	2620.9
	high	0.0% (0/2)	200.27	1.062	49.85	1029.7
	low	0.0% (0/2)	14.68	0.065	2.62	58.0
GPT-6 Astra	max	50.0% (1/2)	151.45	1.054	226.18	1041.4
	high	0.0% (0/2)	27.13	0.118	37.51	114.2

Appendix

Table A12: Results for CCF.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	45.5% (5/11)	108.28	0.788	26.35	538.5
	high	36.4% (4/11)	63.56	0.289	11.00	299.2
	low	45.5% (5/11)	115.43	0.350	19.73	342.1
GPT-6 Astra	max	54.5% (6/11)	131.92	0.716	182.73	918.1
	high	36.4% (4/11)	55.19	0.274	75.18	303.5

Appendix

Table A13: Results for PirateShip.

Model	Effort	Success Rate (pass@3)	Total Tokens (M)		Total Cost	Total Agent Time
Model	Effort	Success Rate (pass@3)	Input	Output	(USD)	(min)
GPT-6.1 Sol	max	0.0% (0/1)	10.53	0.103	2.78	56.9
	high	0.0% (0/1)	9.29	0.064	2.13	42.3
	low	0.0% (0/1)	3.08	0.021	0.82	14.3
GPT-6 Astra	max	0.0% (0/1)	9.29	0.083	16.31	65.0
	high	0.0% (0/1)	7.15	0.050	11.96	134.4

Appendix

Table A14: Results for Wildfire.

Specification	Issue	Repair	Status
OpenAddressing	With a single fingerprint, the divisor max(fps) - min(fps) in the hash rescaling is zero.	Require a finite set of at least two fingerprints.	Fixed upstream
MongoDB	vars omits five of the 25 state variables, so stuttering steps can change them.	Add them to vars .	Fixed upstream
Walgit WAL	Overlapping CASE guards allow replay to skip a checkpoint and omit committed data. Reordering the branches exposes a violation hidden by TLC’s default order.	Make replay and retry guards mutually exclusive.	Reported; no response
MongoDB	One transaction can start at two routers with different read timestamps, violating SnapshotIsolation (Section 4.1 ).	Check all routers before a transaction starts.	Fixed upstream
Sailfish	Correct nodes accept a Byzantine leader’s proposal without a predecessor reference or a no-vote certificate, violating Agreement .	Check the predecessor reference or no-vote certificate before admission.	Fixed upstream
SlateDB WAL	A delayed writer’s fence, written after garbage collection, is skipped during replay, and ConsistentMachineData fails.	Validate the writer’s epoch after replay.	Reported; no response

Appendix

Table A15: Representative specification issues and their repairs.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 171 papers

TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents
Oct 10, 2026Kseniia Strelbytska, Balázs Szilágyi, Anna Mészáros +1Formal Verification Automated Theorem Proving
Stephen Perse Cambridge, UK · University of Cambridge, UK · Reasonable
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Jun 4, 2026Eric Spencer, Arslan Bisharat, Brian Ortiz +6LLM-Based Program Synthesis Formal Verification
Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA
TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation
Jul 26, 2026Arslan Bisharat, Eric Spencer, Brian Ortiz +8LLM Evaluation Formal Verification
Loyola University Chicago Chicago, Illinois, USA

Oct 10, 2026J/K move · Enter open · S save

TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents

Kseniia Strelbytska, Balázs Szilágyi, Anna Mészáros, Ferenc Huszár

Stephen Perse Cambridge, UK · University of Cambridge, UK · Reasonable

Formal Verification Automated Theorem Proving Temporal Reasoning in Language Models LLM-Based Program Synthesis

Open paper AskPDF arXiv

The TLA+ (temporal logic of actions) formal specification toolkit has seen widespread adoption in modeling modern distributed software systems including databases, storage systems, ledgers and coordination protocols. This popularity is despite its two significant limitations for software verification: Firstly, TLA+ offers no way to detect drift between software implementation and mathematical specification; secondly, TLC and TLAPS cannot provide satisfactory proofs of arbitrary temporal logic properties. We address the second limitation and take a first step towards the first by translating TLA+ specifications into Verus, an auto-active verifier built for Rust, via both a deterministic transpiler and an agentic translator. We demonstrate that our LLM-based pipeline is able to generate proof obligations from TLA+ specifications at scale, and to produce fully machine checkable proofs of both safety and liveness properties. Since temporal logic reasoning in Verus is a largely new task for LLMs, our work yields a valuable evaluation dataset, which we use to map out current generation model capabilities in Verus theorem proving.

Abstract

Automated Theorem Proving

Explore similar work

TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents

TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation