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

TLAPS-B ENCH : F ORMALLY P ROVING C ORRECTNESS OF R EAL -W ORLD S YSTEM S PECIFICATIONS WITH TLA+ P ROOF S YSTEM

arXiv:2611.02849v1 [cs.AI] 2 Nov 2026

Qian Cheng 1 Ruize Tang 2 Saad Mohammad Rafid Pial 3 Zhizhen Cathy Cai 3 Yiming Su 3 Jackson Clark 3 Munim Thahmid 4 Mahdiya Rahman Sukanya 5 Chris Newcombe 6 Igor Konnov 7 Stephan Merz 8 Xudong Sun 9 Murat Demirbas 10 Yu Huang 1 Markus Alexander Kuppe 7 Tianyin Xu 3 11

A BSTRACT 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. 1

I NTRODUCTION

Formal proofs establish correctness properties of concurrent and distributed systems, such as cache coherence, consensus agreement, and transaction isolation, across all possible executions. Unlike other formal methods like model checking (Clarke et al., 1986), machine-checked proofs establish these properties deductively, providing correctness guarantees beyond finite exploration (Cousineau et al., 2012). Traditionally, constructing formal proofs requires substantial expertise and effort. Developers must discover suitable inductive invariants (Ma et al., 2019; Yao et al., 2021), prove that they are preserved by every system transition, and decompose the reasoning into proof obligations that automated tools can discharge. For example, proving election safety in a consensus protocol (Ongaro & Ousterhout, 2014) may require strengthening the target property with auxiliary invariants about majority support and vote uniqueness. Recent advances in agentic AI show promise for automating proof construction. Several recent studies demonstrate that agents can construct nontrivial machine-checked proofs through iterative interactions with proof checkers (Lucas 1 Nanjing University 2 Microsoft 3 University of Illinois at Urbana-Champaign 4 Bangladesh University of Engineering and Technology 5 IIT, University of Dhaka 6 Oracle 7 Independent 8 University of Lorraine, CNRS, Inria, Nancy, France 9 University of Toronto 10 MongoDB 11 University of California, Berkeley. Correspondence to: Yu Huang <yuhuang@nju.edu.cn>.

et al., 2026; Yang et al., 2025a;b; Ye et al., 2026a; Agarwal et al., 2026). These advances offer a path toward automating proof development for real-world concurrent and distributed systems beyond prototypes and research artifacts. However, existing benchmarks do not sufficiently address end-to-end proof construction for real-world system specifications. First, many benchmarks provide agents with helper lemmas and intermediate invariants (Yang et al., 2025b; Xin et al., 2026), or with predefined proof decomposition that specifies individual theorems and their dependencies (Zhang et al., 2024; Lin et al., 2024). Such proof-completion style benchmarks predefine much of the proof structure, missing key challenges of discovering auxiliary invariants/lemmas, decomposing the target property into tractable proof obligations, and organizing them into a complete proof. Second, few existing benchmarks target real-world system specifications. Many instead evaluate research artifacts developed specifically with formal verification in mind. For example, both VeruSAGE (Yang et al., 2025b) and Vero (Ye et al., 2026a) include IronKV (Hawblitzel et al., 2015), rather than widely deployed systems such as etcd and MongoDB. It is unclear whether agents can construct proofs for substantially richer behaviors of real-world systems. Lastly, correctness properties of concurrent and distributed systems (e.g., liveness) go beyond functional correctness addressed by existing benchmarks like Vero (Ye et al., 2026a).

1

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

TLAPS-Bench Tasks

TLA+ Proof Harness (Tilapia)

Full collection: 95 specs, 265 tasks Evaluation set: 12 specs, 70 tasks

AI agent

Proof tools

Example Proof Tasks

Example Generated Proof

Spec == Init /\ [][Next]_vars FairSpec == Spec /\ Fairness

1 THEOREM AgentMemInvAlways == 2 Spec => []AgentMemInv 3 ... 4 THEOREM Spec => []MemDataProp 5 BY AgentMemInvAlways, ...

Target properties Spec => []MemDataProp FairSpec => WbProgress

Safety Liveness

Submission Verification Proof checked by TLAPS Counterexample checked by TLC / Apalache

Example Results Verified targets Agent runtime Cost

11 / 15 1981.5 min $186.79

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

Concurrent and distributed systems require extensive reasoning about system-wide properties that emerge from interactions among components over time, such as agreement, consistency, isolation, etc. These properties pose distinct proof challenges, because their correctness depends on the composition and interleaving of many state transitions. We present TLAPS-Bench, a benchmark and execution harness for constructing machine-checked proofs of system and protocol specifications in TLA+ (the de facto formal language for specifying concurrent and distributed systems; see §2). We set two goals for TLAPS-Bench: • building a proof service to verify important real-world systems and protocols that desire correctness guarantees; • understanding the capabilities of frontier AI in constructing formal proofs of real-world systems, end to end. Each task in TLAPS-Bench is a proof target (a property to be proved) desired for a real-world system/protocol, as shown in Figure 1; so, results are of practical value. TLAPS-Bench includes a proof harness for autonomous proof development, named T ILAPIA (TLA+ Proof Infrastructure for Agents). T ILAPIA is built atop the TLA+ Proof System or TLAPS (Cousineau et al., 2012), the native proof system for TLA+ . It provides agents with tools including a semantic analyzer, model checkers, and common proof libraries. Agents can use these tools during proof development to explore system behaviors, refine proofs, and validate proof obligations. For example, agents constantly use model checkers to test invariants and obtain counterexamples that guide proof development. T ILAPIA also enforces safeguards against reward hacking, ensuring that accepted proofs establish target properties under the original specifications. We have used T ILAPIA to construct machine-checked proofs for important properties for real-world system and protocol specifications which were not proved before. TLAPS-Bench maintains a collection of 95 TLA+ specifications and 265 proof targets drawn from real-world systems and protocols, spanning cache coherence, Byzantine fault tolerance, and write-ahead logs. The proof targets cover

safety, liveness, and refinement properties. We are continuously adding new proof tasks and retiring tasks that were proved and can no longer challenge AI frontier. We evaluate frontier AI agents, represented by Codex with GPT models, on 70 proof targets across 12 real-world system specifications. The highest-scoring model, GPT-6.1 Sol at max effort, successfully proves 31 (44.3%) targets, demonstrating strong capability while leaving substantial room for improvement. Our analysis reveals that success depends not only on finding valid proof arguments. For example, case studies show that the choice and decomposition of invariants substantially affect proof obligations, whereas naı̈ve calling of automated backends is ineffective. In summary, we make the following main contributions: • T ILAPIA, an effective TLA+ proof harness for agentic TLA+ proof development, which offers a TLA+ proof service for real-world system specifications; • TLAPS-Bench, a rich benchmark suite for end-to-end proof development based on real-world system specifications, which poses significant challenges to frontier AI; • An analysis of frontier AI’s ability of developing formal proofs for real-world system/protocol specifications. • TLAPS-Bench and T ILAPIA are publicly available at github.com/specula-org/TLAPS-Bench.

2

BACKGROUND

TLAPS-Bench focuses on formally proving the correctness of TLA+ specifications (Lamport, 2002). TLA+ is the de facto specification language for verifying concurrent and distributed systems. It is widely adopted across industry (TLA+ Foundation, 2026) to specify and verify cloud infrastructure (Newcombe et al., 2015; Howard et al., 2025), replication protocols (Ouyang et al., 2025), databases like Azure Cosmos DB and MongoDB (Hackett et al., 2023; Schultz & Demirbas, 2025), OS kernel code (Tang et al., 2025), and hardware cache coherence (Beers, 2008). A TLA+ specification comprises a system model and correctness properties. The model defines a state machine

2

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System 1 1 Model 2 CONSTANTS Server, Follower, Candidate, Leader 3 VARIABLES state, currentTerm, votesGranted, ... 4 \* Initially, every server is a follower in term zero. 5 Init == /\ state = [i \in Server |-> Follower] 6 /\ currentTerm = [i \in Server |-> 0] 7 /\ votesGranted = [i \in Server |-> {}] /\ ... 8 \* Start a new election. 9 Timeout(i) == 10 /\ state[i] \in {Follower, Candidate} 11 /\ currentTerm’ = [currentTerm EXCEPT ![i] = @ + 1] 12 /\ votesGranted’ = [votesGranted EXCEPT ![i] = {}] 13 /\ state’ = [state EXCEPT ![i] = Candidate] /\ ... 14 \* Become leader after receiving a quorum of votes. 15 BecomeLeader(i) == 16 /\ state[i] = Candidate 17 /\ votesGranted[i] \in Quorum(GetConfig(i)) 18 /\ state’ = [state EXCEPT ![i] = Leader] /\ ... 19 Next == \E i \in Server: 20 Timeout(i) \/ BecomeLeader(i) \/ ... 21 Spec == Init /\ [][Next]_vars 22 23 2 Target No two different servers lead in the same term. 24 LeaderUniqueness == \A i,j \in Server: 25 currentTerm[i] = currentTerm[j] 26 /\ state[i] = Leader /\ state[j] = Leader => i = j 27 THEOREM LeaderUniquenessTheorem == 28 Spec => []LeaderUniqueness

1 3 Proof 2 \* Introduce a stronger election invariant. 3 ARInv == /\ ... \* unique vote per voter and term 4 /\ \A i \in Server: state[i] = Leader => 5 votesGranted[i] \in Quorum(GetConfig(i)) 6 LEMMA ARInitial == Init => ARInv 7 ... \* holds in every initial state 8 LEMMA ARStep == ARInv /\ [Next]_vars => ARInv’ 9 ... \* preserved by every step 10 LEMMA ARAlways == Spec => []ARInv 11 <1>1. Init => ARInv BY ARInitial 12 <1>2. ARInv /\ [Next]_vars => ARInv’ BY ARStep 13 <1>3. QED BY <1>1, <1>2, PTL DEF Spec 14 \* Quorum intersection gives a unique leader. 15 LEMMA ARUniqueLeader == ARInv => LeaderUniqueness 16 <1>1. ASSUME ARInv, NEW i,j \in Server, 17 currentTerm[i] = currentTerm[j], 18 state[i] = Leader, state[j] = Leader 19 PROVE i = j 20 <2>1. votesGranted[i] \cap votesGranted[j] # {} 21 BY <1>1, ARQuorumsIntersect 22 <2>2. QED BY <1>1, <2>1 23 <1>2. QED BY <1>1 DEF LeaderUniqueness 24 THEOREM LeaderUniquenessTheorem == 25 Spec => []LeaderUniqueness 26 <1>1. Spec => []ARInv BY ARAlways 27 <1>2. ARInv => LeaderUniqueness BY ARUniqueLeader 28 <1>3. QED BY <1>1, <1>2, PTL

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).

through a set of state variables, an initial predicate that defines their initial values, and a next-state relation written as a collection of actions, each describing one atomic update to the variables. Correctness requirements are expressed as temporal properties, including safety (nothing bad ever happens) and liveness (something good eventually happens). TLA+ is built upon the Temporal Logic of Actions (TLA) (Lamport, 1994), which extends linear temporal logic (Pnueli, 1977) to express models and temporal properties in a single logic. A target theorem asserts that every behavior allowed by the model satisfies a given property. TLA+ specifications can be validated through explicit-state model checking with TLC (Yu et al., 1999) and symbolic model checking with Apalache (Konnov et al., 2019), or verified via deductive verification with the TLA+ Proof System (TLAPS) (Cousineau et al., 2012). Model checking can expose counterexamples through finite-state or bounded exploration, but its guarantees are limited to the configured bounds. Deductive verification can establish a target theorem beyond those bounds by checking a proof. In TLAPS-Bench, agents construct complete TLA+ proofs of these theorems. TLAPS checks these proofs by generating proof obligations for their steps and dispatching them to specialized backends, including SMT solvers such as Z3 (de Moura & Bjørner, 2008), Isabelle/TLA+ (Paulson, 1994), and LS4 (Suda & Weidenbach, 2012). Agents may use TLC and Apalache to test candidate invariants and obtain counterexamples that guide proof development, but a

target is accepted only when TLAPS verifies the proof. Figure 2 illustrates the input and output of an etcd Raft task in TLAPS-Bench. The input on the left consists of a system model and a target property, while the output on the right is an accepted agent-generated TLAPS proof. Init defines the initial states, in which every server is a follower in term zero and has received no votes. Timeout initiates a new election by transitioning a server to the candidate state, advancing its term, and resetting its votes; BecomeLeader transitions a candidate with a quorum of votes to the leader state. Next combines these with the remaining actions, and Spec defines the allowed system behaviors. The target LeaderUniqueness states that two leaders in the same term must be the same server, and the theorem Spec => []LeaderUniqueness asserts that this property always holds (the temporal operator [] denotes “always”). The output on the right proves the target property through a stronger inductive invariant. This invariant, ARInv, captures voting facts needed by the proof but not stated in LeaderUniqueness: every leader has votes from a quorum, and each voter supports at most one candidate in a term. ARInitial and ARStep establish that ARInv holds initially and is preserved by every action. Using these lemmas, ARAlways proves Spec => []ARInv. To derive the target, ARUniqueLeader applies quorum intersection: two leaders in the same term must share a voter, whose vote uniqueness implies that they are the same server. Together, these results establish Spec => []LeaderUniqueness.

3

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

While TLA+ and TLAPS are built natively around TLA, state-machine and temporal reasoning can also be realized in other proof systems. Lean (de Moura & Ullrich, 2021) targets general theorem proving and supports state-machine verification with Veil (Pı̂rlea et al., 2025), while Verus (Lattuada et al., 2024) targets Rust verification and encodes temporal reasoning through libraries (Sun et al., 2024; Cai et al., 2026). TLAPS-Bench focuses on TLA+ , but the techniques can be extended to other proof systems.

3

T ILAPIA : TLA+ P ROOF H ARNESS

We develop T ILAPIA: a TLA+ proof harness, to support AI agents for autonomous development of TLA+ proofs. T ILAPIA provides agents with the flexibility to develop proof strategies, invoke verification tools, and build on partial progress, while preventing reward hacking and ensuring that accepted proofs establish the original targets. Using T ILAPIA, we have instructed AI agents to construct machine-checked proofs for TLA+ specifications of important systems and protocols. Table 1 gives a few examples where we proved the target properties for the TLA+ specifications, including both classic protocol and real-world system specifications (some of them had proofs in other forms). For example, Bosco (Song & Renesse, 2008), an asynchronous Byzantine consensus protocol, only has penand-paper proofs; we generated TLA+ proofs for its five properties. We also proved all the properties of several WAL (Write Ahead Log) protocols of databases; these protocols were specified in TLA+ and heavily model checked, but were not formally proved to be correct. T ILAPIA organizes each proof target as a task and groups tasks of the same specification in one proof file, allowing their proofs to share auxiliary invariants and lemmas. For proof integrity (see §3.2), the TLA+ model and the target properties are placed in separate read-only files. Within the proof file, target theorem statements are fixed, while agents can define auxiliary invariants and lemmas in a shared editable region and construct a proof for each target. This layout preserves the original proof goals while allowing agents to flexibly choose their own proof strategies. T ILAPIA uses Docker containers to isolate workspaces of different agents. File-system isolation mounts the original task files read-only and each run starts a fresh agent session without conversations or memories from other runs; network isolation only allows connections to LLM API endpoints and agent built-in web search tools are disabled. 3.1

Tools for Agents

T ILAPIA provides a local environment for agents to construct proofs of target properties in a TLA+ specification. It supports coding agents such as Codex, Claude Code, Copi-

Table 1. Examples of TLA+ specifications we proved using T ILAPIA. Some of them were proved in other forms. Specification

LOC

Targets

German protocol Bosco Byzantine consensus Sailfish BFT consensus OSWALD WAL SlateDB WAL Walgit WAL TLC DiskStateQueue Disruptor MPMC Disruptor SPMC BufferedRandomAccessFile

402 140 200 260 564 558 1,567 215 187 334

7 5 3 3 4 7 1 2 2 14

Prior Proof Isabelle Pen-and-paper Rocq None None None None None None None

TLC

AI agent

model checker

Candidate invariant

Exactly one node has the token.

check

Violation found feedback

Counterexample an execution trace that violates the candidate A sends it B A A has the token refine Refined candidate invariant

Exactly one node or in-transit message has the token.

B A in transit: no node has it

check again

No violation

in any state of the 2-node system

Proof construction for any number of nodes

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.

lot, and Cursor, and integrates pinned versions of SANY for semantic analysis, TLAPS for proof checking, and TLC and Apalache for model checking. T ILAPIA provides agents with the TLAPS library (Chaudhuri et al., 2026) and CommunityModules (Kuppe et al., 2026) which include theorems and proofs for commonly used TLA+ operators, such as set and sequence operations. Model checkers. T ILAPIA provides model checkers, including TLC (Yu et al., 1999) and Apalache (Konnov et al., 2019), to help agents test conjectures during proof development. TLC explores reachable states of a finite model, while Apalache uses SMT solving for bounded exploration and inductiveness checking. Both can quickly falsify incorrect conjectures by producing counterexamples. An agent can use them to test whether a proposed invariant holds and use a counterexample to identify conditions needed to refine it, as illustrated in Figure 3. Model checking thus provides rapid feedback for proof development, while the final proof is established by TLAPS.

4

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

Guidance. T ILAPIA provides two agent skills to guide the use of proof libraries and model checkers. The first explains how to apply instantiated library theorems, e.g., by establishing the premises required to use them. The second explains how to configure invariant checks, e.g., by using the proposed invariant as the initial predicate when checking its preservation. Both address common usage errors that agents encounter without explicit guidance. Proof checker. Agents can invoke the same TLAPS proof checker used for final evaluation, with identical acceptance criteria and per-verification time limits. The checker provides two modes: (1) a fast pass runs SANY for immediate syntax and semantic feedback, while (2) a full pass applies the proof-integrity checks of §3.2 and then verifies each target together with its dependencies. For each target, the checker reports whether its proof succeeded, failed, or exceeded the time limit. This feedback helps agents identify unresolved proof obligations, repair failed proofs, and decide where to focus subsequent proof development. 3.2

Proof Integrity

ASSUME Useful == FALSE THEOREM Spec => []Agreement BY Useful

(a) Added assumption. ZooKeeper’s agreement proof assumes FALSE. LEMMA NextInv == IndInv /\ [Next]_vars => IndInv’ PROOF OMITTED ... THEOREM Spec => []Leadership1 ... <1>2. IndInv /\ [Next]_vars => IndInv’ BY NextInv

(b) Unproved helper. ZooKeeper’s leadership proof cites an unproved NextInv. Replaced file: /opt/tlapm/bin/tlapm #!/bin/bash echo ’[INFO]: All 214 obligations proved.’ exit 0

(c) Checker tampering. A fake tlapm yields a local PASS. Figure 4. Three cheating attempts observed in real agent runs that can appear successful without T ILAPIA.

T ILAPIA accepts a proof for a target property if all three of the following conditions hold: • Context integrity. The proof must establish the target property under the original specification and assumptions. For example, in Figure 4(a), an agent adds ASSUME Useful == FALSE, making ZooKeeper’s agreement theorem trivially provable. T ILAPIA therefore makes the specification and target theorems read-only and restricts edits to designated regions of the task file. Within these regions, SANY’s semantic analysis is used to permit only definitions, named lemmas, and imports from pinned proof libraries, while rejecting new assumptions, axioms, constants, and variables. In summary, agents can introduce auxiliary invariants and lemmas without changing the logical context in which the target must be proved. • Dependency tracking. Every lemma on which a target depends must itself be proved. Figure 4(b) shows a direct violation: the proof of ZooKeeper’s leadership property cites NextInv, but the proof of NextInv is omitted. More subtly, because targets are verified separately for evaluation (§5.1), a target may pass even when the proof of a helper lemma it cites fails. Without tracking such dependencies, an agent could therefore establish a target by relying on an unproved or unprovable lemma. T ILAPIA uses SANY to extract lemma references and constructs a dependency graph over targets and helper lemmas. A target is accepted only if its own proof succeeds and every lemma on which it transitively depends is also proved. • Clean-room grading. The final result must be independent of any agent-modifiable tools or execution environment. In Figure 4(c), an agent replaces tlapm with

a script that simply reports success, causing the local checker to return PASS without verifying the proof. To prevent such manipulation, T ILAPIA grades each submission in a fresh container with the original task files and unmodified verification tools, carrying over only the submitted task module. Agents may create wrapper modules, configuration files, and scripts during proof development, but these artifacts are excluded from the grading environment and therefore cannot affect the final result. 3.3

Execution Control

T ILAPIA enforces fixed verification time limits and CPU quotas to ensure consistent execution conditions across runs. It tracks resource usage including execution time, token usage, model cost, and tool calls, enabling evaluation of both proof success and computational cost. To support long-running experiments, T ILAPIA can pause and resume agent runs interrupted by external failures, such as provider quota limits or API outages. Resumed runs retain completed verification results and caches, avoiding redundant computation while preserving the agent’s progress.

4

TLAPS-B ENCH

The proof tasks from TLAPS-Bench come from TLA+ specifications of real-world systems and protocols. TLAPSBench currently includes 95 specifications with 265 proof targets, covering cache coherence, distributed consensus, atomic broadcast, transaction isolation, and concurrent data

5

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System 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. Specification FLASH Cache coherence ZooKeeper protocol Cahill’s serializable snapshot isolation Ivy TLB OpenAddressing etcd Raft HashiCorp Raft ZooKeeper implementation MongoDB distributed transactions CCF Raft PirateShip consensus Wildfire cache coherence∗

Type Protocol Protocol Protocol System System System System System System System Protocol Protocol

Model Source TLA Specification Repository Remix (Ouyang et al., 2025) Amazon Snapshot Spec Ivy examples TLA+ Specification Repository Specula (Cheng et al., 2026a) Specula (Cheng et al., 2026a) Remix (Ouyang et al., 2025) MongoDB Research Microsoft CCF (Howard et al., 2025) PirateShip (Mishra et al., 2026) Wildfire Challenge (Lamport et al., 2001)

structures. In the spirit of measuring the frontier (and saving token cost), we maintain an active set of challenging proof tasks and retire tasks that are too easy for AI agents. Our current active set has 12 specifications with 70 targets and we will use this set in our evaluation. The information of the other tasks can be found in Appendix A. 4.1

Spec LOC

+

Task Definition

In TLAPS-Bench, a task is to prove a target property of a given TLA+ specification. Targets include safety, liveness, and refinement properties. A safety property rules out undesirable behaviors—any violation can be witnessed by a finite execution prefix, such as two processes simultaneously accessing a shared resource without protection. A liveness property requires progress over an execution, such as every pending request eventually completing; unlike safety, its violation cannot be established from any finite prefix because the required event may still occur later. A refinement property relates two specifications, requiring every behavior of a concrete model, under a refinement mapping, to satisfy an abstract specification. For example, Wildfire’s refinement target requires its request and response histories to satisfy the Alpha memory model (Lamport et al., 2001). A specification consists of a formal TLA+ model, which defines state variables and actions, and the targets as TLA+ theorems, stating what properties the model should satisfy. Figure 2 shows one task from etcd Raft: the formal model defines state variables and election actions, while the target LeaderUniqueness states that two leaders in the same term must be the same server. Note that the TLA+ specifications are not guaranteed to be correct. As they are collected from real-world systems/protocols (some were generated by tools (Cheng et al., 2026a) that infer TLA+ specifications from source code), many of them were not formally proved though most of them have

623 994 407 361 356 601 656 1,840 724 1,144 586 1,251

Targets 15 (Safety + Liveness) 9 (Safety) 1 (Safety) 2 (Safety + Liveness) 5 (Safety) 8 (Safety) 6 (Safety) 9 (Safety) 1 (Safety) 2 (Safety) 11 (Safety) 1 (Refinement)

been heavily model checked. It is possible that specifications are incorrect—either the system designs are flawed or the specification was not written correctly. In either case, the results of TLAPS-Bench help improve real-world system specifications and/or their designs/implementations. During task construction, we found 46 specification issues, of which 35 have been fixed. For example, an agent found a snapshot isolation violation in MongoDB’s TLA+ specification which incorrectly allowed one transaction to use two routers with different read timestamps; the model checking uses a single-router configuration and thus misses it. For the target property of a given task, the AI agent either proves it to be correct by providing a proof that can pass T ILAPIA’s proof checks (§3), or disproves it by providing a counterexample that shows an execution that violates the target property. The counterexample can be generated using model checkers like TLC or Apalache. TLAPS-Bench poses few restrictions on the proof strategies: agents can pick their own auxiliary invariants and use the tools, libraries, and guidance provided by T ILAPIA. 4.2

Task Construction

Some specifications list explicit correctness properties. In this case, each property P of a specification Spec is formulated as a top-level theorem in the form of Spec ⇒ P . For example, the German protocol’s theorem Spec => []Coherence states that exclusive access to a cache line cannot coexist with access by another cache. AI agents are asked to prove the theorem end-to-end. If the specification contains proofs of the target theorem, we carefully remove all related auxiliary lemmas and proofs. For specifications that do not have explicit properties, we identify target properties from different sources. If a model checking configuration lists a property as an invariant, such as OpenAddressing’s Sorted invariant described in its

6

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System \* Model checking configuration CONSTANT RC = "snapshot" IgnorePrepareBlocking = "false" IgnoreWriteConflicts = "false"

# Ivy assume pc_i1(p); pc_i2(p) := true; pc_i1(p) := false;

\* TLAPS expansion bug LET ps == [x \in ss |-> {Append(sq, x) : sq \in perms[ss \ {x}]}] IN UNION {ps[x] : x \in ss}

ASSUME SnapshotConfiguration == /\ RC = "snapshot" /\ IgnorePrepareBlocking = "false" /\ IgnoreWriteConflicts = "false"

/\ pc[p] = InitiatorDeactivate /\ pc’ = [pc EXCEPT ![p] = InitiatorLockPmap]

UNION {{Append(sq, x) : sq \in perms[ss \ {x}]} : x \in ss}

(a) Explicit assumptions. MongoDB’s model checking settings become assumptions in the proof task.

(b) Language translation. An excerpt from translating Ivy’s TLB shootdown model into TLA+ .

(c) Tool compatibility. Inlining a nested binding in MongoDB’s PermSeqs avoids incorrect expansion in TLAPS.

Figure 5. Three examples of rewriting specifications into TLAPS-Bench tasks. OpenAddressingModel.tla ASSUME ... \* Assumptions Read-only \* Model actions and behaviors Init == ... Next == ... EXTENDS Sequences, Spec == ... FiniteSets, Integers \* Helper; not needed by targets CasFreshnessCore == ... Extract \* Keep model context ASSUME ... \* Assumptions isSorted(seq) == ... Init == ... Sorted == Next == ... isSorted(external) /\ Spec == ... isSorted(newexternal) THEOREM Spec => []Sorted \* Target

OpenAddressingDefs.tla Read-only

OpenAddressing.tla Green part is writable

\* Reuse model context EXTENDS OpenAddressingModel

EXTENDS OpenAddressingDefs

\* Keep target context isSorted(seq) == ... Sorted == isSorted(external) /\ isSorted(newexternal)

\* New helper region THEOREM Spec => []Sorted \* Reset the source proof PROOF OMITTED

Figure 6. An example of task organization of the OpenAddressing specification.

.cfg file, we formulate the target Spec => []Sorted. If correctness requirements are stated in other files, such as comments and documents, as in the Cahill SSI specification whose comments say that serializability must hold, we formulate targets from those requirements as Spec => []CahillSerializable(history). Rewriting specifications. Certain revisions of the specification may be needed, including rewriting constructs for tool issues, and adding explicit assumptions specified in other sources. We also translate specifications written in other specification languages into TLA+ . Figure 5 shows three examples. 5(a) shows MongoDB’s snapshot isolation specification whose model-checking configuration encodes assumptions as constant assignments. We make these assumptions explicit in the proof task. 5(b) shows our translation of a TLB specification from Ivy to TLA+ . We map Ivy state and transitions to TLA+ variables and actions, and use TLC to check the translated specification on a finite instance. 5(c) shows an incorrect TLAPS expansion of a nested LET inside a definition of a recursive function. We work around this issue by inlining the binding without changing the recursive function or its domain. Task organization. As a final step, we transform each specification into the task format expected by T ILAPIA (§3). We use SANY, the TLA+ syntactic analyzer, to resolve references and compute the transitive dependencies of each target theorem. Figure 6 illustrates this process for the Sorted theorem in OpenAddressing. The statement Spec

=> []Sorted depends on Spec, Sorted, and, transitively, isSorted; we retain the union of such dependencies across all selected targets. We remove definitions outside this dependency closure, together with existing proofs, auxiliary lemmas, unselected theorems, and comments. The retained content is then organized into three modules. OpenAddressingModel.tla contains the specification and assumptions, while OpenAddressingDefs.tla contains the target properties and their definitions, e.g., Sorted and isSorted; both modules are read-only. The editable task module, OpenAddressing.tla, contains the target theorem statements and regions for agents to introduce helper definitions, lemmas, and proofs. Targets from the same module share a task file and helper region, allowing agents to develop and reuse common lemmas. 4.3

Task Validation

Unlike agentic coding benchmarks that validate generated programs by running test cases, the validation of agent results in TLAPS-Bench is complete with no ambiguity. For each task, an agent succeeds by proving the target to be either correct (with a formal proof) or wrong (with a counterexample). An agent fails if it can neither prove the target nor provide a counterexample. The validation does not depend on test coverage, hidden test cases, or an approximate correctness oracle. As with other formal techniques, the guarantee is relative to the trusted computing base, including TLAPS and its backends (e.g., Z3, Isabelle, and LS4).

7

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System Table 3. Overall benchmark results on the problem set described in Table 2. Success Rate Total Cost Correct Proof LOC Total Tokens (M) (pass@3) (USD) Total Per Target Input Output

Total Agent Time (min)

Model (Agent)

Effort

GPT-6.1 Sol (Codex)

max high low

44.3% 34.3% 35.7%

15,619 5,967 8,834

503.8 248.6 353.4

1456.14 635.57 549.23

7.730 3.312 2.238

$328.86 $134.75 $97.75

5917.4 2725.0 1795.6

GPT-6 Astra (Codex)

max high low

42.9% 34.3% 34.3%

13,725 5,503 7,175

457.5 229.3 299.0

770.22 353.11 272.83

4.270 1.663 1.162

$1086.44 $486.57 $373.41

3992.5 1575.7 1262.5

GPT-5.6 Terra (Codex)

max high low

21.4% 0.0% 0.0%

15,448 -

1,029.9 -

21475.87 126.85 35.45

56.232 0.635 0.243

$5602.15 $42.00 $14.78

52481 528.6 215.2

GPT-6 Luna (Codex)

max high low

10.0% 0.0% 0.0%

11,497 -

1,642.4 -

2338.15 33.98 13.81

9.586 0.284 0.070

$31.11 $0.69 $0.30

5285.4 200.3 45.6

Developing and evaluating TLAPS-Bench has also led to improvements to TLAPS itself, including bug fixes and support for autonomous proof development. For example, we introduced a strict mode that treats missing or omitted proof steps as errors, allowing T ILAPIA to ensure that submitted proofs are complete rather than relying on unproved steps.

5

E VALUATION

5.1

Experimental Setup

We evaluate the latest available GPT models: GPT-6 Astra, GPT-6.1 Sol, GPT-6 Luna, and GPT-5.6 Terra. We use Codex across the models with max, high, and low reasoning effort (12 configurations in total). The evaluation ran on an Ubuntu 24.04.3 virtual machine with 96 vCPUs, backed by an AMD EPYC 9V74 processor and 378 GiB of DRAM. Each run executed in a separate Docker container with 8 vCPUs. We set a time limit of 60 minutes for the TLAPS backend to process a proof, which is empirically sufficient for properly decomposed proofs to be verified. We also set a cumulative limit of two million output tokens (including reasoning tokens) for each specification. Only Terra and Luna at max effort reach this limit (they could not finish the proof but did not give up). Metrics. We report pass@3, the fraction of tasks that pass in at least one of three independent runs, to accommodate nondeterminism. We report input/output token usage, model cost, and agent execution time (including model prompting and tool calling), summed across all tasks and all three runs. 5.2

Proof Capability

Table 3 shows significant differences in proof capability across evaluated models. GPT-6.1 Sol achieves the highest success rate at max effort, proving 31 of 70 targets (44.3%),

followed closely by GPT-6 Astra with 42.9%. GPT-5.6 Terra and GPT-6 Luna prove far fewer targets at max effort and none at high or low effort. The successful proofs show that frontier AI agents can establish correctness properties of real-world specifications. Astra and Sol proved all 15 targets of the FLASH cache coherence protocol, spanning both safety and liveness properties. Sol proved all target properties of OpenAddressing. On the other hand, complex tasks are still challenging for frontier AI agents to prove end to end. For example, Sol at max effort proved leader uniqueness and log matching for the etcd Raft system specification, but failed to prove consistency between committed logs and durability of committed entries. For both ZooKeeper protocol and system specifications, Sol proves none of the target properties. System specifications introduce additional proof challenges by exposing implementation mechanisms and optimizations abstracted away by protocol specifications. For example, the ZooKeeper protocol specification synchronizes a replica by copying the leader’s entire log, whereas the system specification can send missing log entries, truncate divergent entries, or transfer snapshots. These mechanisms introduce additional states and transitions over which invariants must be preserved, increasing the complexity of the proof. Sol and Astra achieve similar pass@3 scores but exhibit distinct proof-development patterns. On OpenAddressing, Sol persistently strengthens invariants and repairs failed proof obligations until all target properties are proved. In contrast, Astra proves the completion and sortedness properties but terminates with several induction steps unresolved in all three runs, despite remaining token budget. On ZooKeeper, however, Astra constructs a compact invariant abstraction that avoids extensive reasoning about transaction histories and proves leadership properties that Sol leaves unresolved

8

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System Table 4. GPT-6.1 Sol by reasoning effort: total requests and cost over three runs, and mean reasoning tokens per request. Succ. Rate Model Reasoning Cost Spec (pass@3) Effort Requests Tokens (USD) Cahill SSI

0/1 0/1 0/1

low high max

72 196 277

207 442 727

0.81 4.32 8.01

FLASH

15/15 15/15 15/15

low high max

1,400 691 788

389 499 630

36.96 24.92 37.27

(§5.5). These results suggest that Sol is more persistent in iterative proof development, whereas Astra can reduce proof complexity by discovering effective invariant abstractions. This ability to construct simpler proofs, together with earlier termination when proof attempts stall, helps explain why Astra achieves nearly the same overall score while using roughly half as many input and output tokens as Sol. 5.3

Reasoning Effort and Cost

As shown in Table 3, all models achieve their highest success rates at max effort, while low and high effort can perform similarly. Sol performs slightly better at low than high due to one PirateShip target, while Astra achieves identical success rates at low and high effort. The cost often depends on whether or not proof succeeds, as shown in Table 4. On Cahill SSI (unproved), Sol uses both more reasoning tokens per request and more model requests as effort increases. In contrast, on FLASH (solved at every effort), high and max effort require roughly half as many requests as low effort while achieving the same pass@3. Despite using more reasoning tokens per request, high effort has the lowest total cost. Model pricing makes cost distinct from resource usage. Astra (high) uses fewer input and output tokens and produces shorter proofs than Sol (high), yet costs approximately 3.6 times as much. Across all three effort levels, Sol matches or exceeds Astra’s proof success at lower model cost. 5.4

Failure Analysis

Table 5 categorizes failures across three runs. Errors exposed directly by tool feedback, such as invalid counterexamples, syntax or semantic errors, task-preservation violations, and verification timeouts, are relatively rare in final submissions. Stronger models such as Astra and Sol rarely have basic syntax and task-preservation errors. More substantive failures arise from proof construction. In 537 attempts, agents delegate entire target proofs to automated backends without decomposing them into tractable obligations, often after their own proof attempts stall. Most

Table 5. Failure categories across failed proof tasks (pass@3). Category Incorrect counterexample claims Syntax or semantic errors detected by SANY Task preservation violations Verification timeout Undecomposed proof attempts Incomplete proofs

Attempts 9 31 15 21 537 1,455

failures, however, are incomplete proofs: agents fail to discover inductive invariants strong enough to establish the target, or prove helper lemmas without completing the argument connecting them to the target property. 5.5

Case Studies

TLAPS-Bench enables the understanding of effective proof development practices and recurring limitations of existing agents, providing insights for designing more capable proof agents. We present three case studies. ZooKeeper system specification (Astra: ✓; Terra: ✗). The specification has two leadership properties: each epoch has at most one active leader, and leaders recorded at different times within the same epoch must be the same server. Proving these properties is complicated by system state for log synchronization, message queues, and snapshot handling, whose updates span many different actions. GPT-5.6 Terra (max) attempted both properties by developing a large set of invariants over transaction origins, queued messages, and synchronization state. It exhausted the outputtoken budget and failed to prove either target, despite generating roughly 13,000 lines of intermediate proofs. GPT-6 Astra successfully proved both properties. Astra abstracts the state relevant to leadership. Its key invariant treats recorded votes and eligible acknowledgments in transit uniformly as claims of support for a leader. Astra then shows how each protocol action preserves these claims, allowing synchronization and broadcast actions to share a common proof argument. This abstraction proves both leadership properties. The case shows how abstractions can substantially reduce proof complexity. Cahill’s serializable snapshot isolation (Astra: ✗). Astra fails to prove serializability for Cahill SSI despite developing a promising proof strategy. It reduces serializability to a ranking argument: under conditions on transaction order and conflict flags, a ranking function increases along every dependency edge, ruling out cycles. It successfully proves the supporting lemmas but delegates the entire invariantpreservation argument to a single SMT call (Figure 7). This remaining obligation requires substantial protocol reasoning. Committing a transaction, for example, can force

9

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System <1>1. Init => CSInvariant

PROVED

<1>2. CSInvariant /\ Next => CSInvariant’ BY CSB!SMTT("r5") DEF CSInvariant, Next

UNPROVED

One SMT call for all actions returned unknown. <1>4. CSInvariant => CahillSerializable(history)

PROVED

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

other transactions to abort while updating history, locks, and conflict flags. The proof must show that these updates preserve the conditions required by the ranking argument. Rather than decomposing this reasoning into smaller obligations, Astra repeatedly submits the same unresolved obligation to the backend. The supporting lemmas therefore pass verification, but the target theorem remains unproved. Finding a proof strategy is insufficient without decomposing it into obligations that automated backends can discharge. Wildfire challenge (all models: ✗). Wildfire is a cachecoherence protocol whose specification must refine the Alpha memory model. The proof must relate each read to its source write or initial memory and establish an ordering of concurrent operations permitted by the memory model, while preserving these relationships across protocol actions. No evaluated model completed the refinement proof at any effort level. Astra and Sol established basic invariants over request and response records and recognized the need for histories and ordering relations, but failed to construct the invariants connecting protocol executions to the memory model. Luna and Terra made less progress, establishing only basic facts about types and initial states. In its strongest attempt, Sol proved that protocol actions preserve the structure of request and response records and split the refinement proof into executions with and without requests. The no-request case passed verification, but the general case still required history and ordering invariants connecting returned values and concurrent operations to the Alpha memory model. Thus, the decomposition discharged a special case without simplifying the refinement argument.

6

R ELATED W ORK

TLAPS-Bench evaluates AI agents on developing TLA+ proofs for real-world system specifications, end-to-end. We discuss two related lines of work: (1) software verification benchmarks and (2) TLA+ related benchmarks. Software verification benchmarks. Existing benchmarks often evaluate proof completion tasks, which give parts of the proof structure. NTP4VC (Xu et al., 2026) supplies ver-

ification conditions, while DafnyBench (Loughridge et al., 2024) and AutoVerus (Yang et al., 2025a) evaluate proving functions. Several benchmarks build on larger verified systems: Selene (Zhang et al., 2024) and FVELer (Lin et al., 2024) extract Isabelle lemmas from seL4, CoqStoq (Thompson et al., 2024) and VeriSoftBench (Xin et al., 2026) extract theorems from verified Rocq and Lean projects, and Laurel (Mugnier et al., 2025), RVBench (Zhong & Si, 2025), and VeruSAGE-Bench’s main setting (Yang et al., 2025b) extract functions and lemmas from verified systems. Differently, TLAPS-Bench evaluates end-to-end proof construction for TLA+ system specifications. Several other benchmarks also require agents to prove from scratch, including Vero proof-only mode (Ye et al., 2026a), VERINA (Ye et al., 2026b), and VeruSAGE-Bench (Yang et al., 2025b) no-lemma mode. These benchmarks primarily focus on functional properties of individual functions, APIs, or modules. TLAPS-Bench instead targets system-wide properties of concurrent and distributed systems that emerge from interactions among components over time. TLA+ benchmarks. Most benchmarks evaluate AI agents on generating TLA+ specifications from code (Chen et al., 2026; Cheng et al., 2026b) or from natural language descriptions (TLAi+Bench, 2026; Bisharat et al., 2026b;a; Cao et al., 2025). For TLA+ proofs, LMGPA (Zhou & Tripakis, 2026) includes a benchmark for proof decomposition; the focus is to evaluate LLMs on discovering subclaims recursively. However, the LMGPA benchmark does not evaluate TLA+ proofs end-to-end, e.g., AI agents are supplied with inductive invariants in LMGPA. TLA-Verus (Strelbytska et al., 2026) also includes a related benchmark. The benchmark is on Verus, where specifications were translated from TLA+ . TLA-Verus had an incorrect understanding of TLAPS, saying TLAPS cannot prove arbitrary temporal logic properties. TLAPS decomposes proofs and dispatches obligations to different backends, including LS4 for propositional temporal reasoning. TLAPS-Bench focuses on TLA+ specifications, instead of translated representations.

7

C ONCLUSION AND D ISCUSSION

TLAPS-Bench and T ILAPIA provide infrastructure for AI agents to construct formal proofs of TLA+ system specifications. Proof construction discovers inductive invariants and lemmas that explain why systems are correct and can expose unexpected behaviors or weaknesses in the stated properties. Looking forward, we believe abstraction will be key to scaling proofs: rather than reasoning directly over detailed system models, agents can recover high-level designs and establish refinement across successive abstraction layers. With AI greatly lowering the cost of formal proofs, specifications and proofs could become not only verification artifacts, but also durable representations of system design.

10

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

R EFERENCES Agarwal, S., Krentsel, A., Liu, S., Cemri, M., Cheng, A., Meng, R., Pfister, T., Li, C.-L., Ratnasamy, S., Parameswaran, A., Zaharia, M., Stoica, I., and Lesani, M. Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems. arXiv:2605.23109, May 2026. Beers, R. Pre-RTL Formal Verification: An Intel Experience. In Proceedings of the 45th Annual Design Automation Conference (DAC), June 2008. Bisharat, A., Ortiz, B., Spencer, E., Bhadauria, K., Wang, T., Thiruvathukal, G. K., Läufer, K., and Abuhamad, M. Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation. arXiv:2606.05792, June 2026a. Bisharat, A., Spencer, E., Ortiz, B., Bhadauria, K., Nazari, M., Santos, B., Ramos, A., Wang, T., Thiruvathukal, G. K., Läufer, K., and Abuhamad, M. TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation. arXiv:2607.23425, July 2026b. Cai, Z. C., Date, N., Gu, J. T., Rivera, C., Chajed, T., Padon, O., Xu, T., and Sun, X. Welder: Compositional Liveness Verification of Cluster Control Planes. In Proceedings of the ACM SIGOPS 32nd Symposium on Operating Systems Principles (SOSP), September 2026. Cao, J., Lu, Y., Li, M., Ma, H., Li, H., He, M., Wen, C., Sun, L., Zhang, H., Qin, S., Cheung, S.-C., and Tian, C. From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (ACL), July 2025. Chaudhuri, K., Cousineau, D., Doligez, D., Lamport, L., Libal, T., Merz, S., Tristan, J.-B., and Vanzetto, H. TLAPS Library. https://github.com/tlaplus/ tlapm/tree/main/library, 2026. Chen, Z., Cao, J., Wu, J., Xu, C., and Cheung, S.-C. Can Large Language Models Model Programs Formally? arXiv:2604.01851, April 2026. Cheng, Q., Pial, S. M. R., Tang, R., Su, Y., Ma, E., Hackett, F., Beschastnikh, I., Huang, Y., and Xu, T. Specula: Scaling Formal Specifications for Autonomous Model Checking of System Code. arXiv:2607.25333, July 2026a. Cheng, Q., Tang, R., Ma, E., Hackett, F., He, P., Su, Y., Beschastnikh, I., Huang, Y., Ma, X., and Xu, T. SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems. In Proceedings of the 14th

International Conference on Learning Representations (ICLR), April 2026b. Clarke, E. M., Emerson, E. A., and Sistla, A. P. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), April 1986. Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., and Vanzetto, H. TLA+ Proofs. In Proceedings of the 18th International Symposium on Formal Methods (FM), August 2012. de Moura, L. and Bjørner, N. Z3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2008. de Moura, L. and Ullrich, S. The Lean 4 Theorem Prover and Programming Language. In Proceedings of the 28th International Conference on Automated Deduction (CADE), July 2021. Hackett, F., Rowe, J., and Kuppe, M. A. Understanding Inconsistency in Azure Cosmos DB with TLA+. In Proceedings of the 45th International Conference on Software Engineering: Software Engineering in Practice (ICSESEIP), May 2023. Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J. R., Parno, B., Roberts, M. L., Setty, S., and Zill, B. IronFleet: Proving Practical Distributed Systems Correct. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP), October 2015. Howard, H., Kuppe, M. A., Ashton, E., Chamayou, A., and Crooks, N. Smart Casual Verification of the Confidential Consortium Framework. In Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI), April 2025. Konnov, I., Kukovec, J., and Tran, T.-H. TLA+ Model Checking Made Symbolic. Proceedings of the ACM on Programming Languages (PACMPL), October 2019. Kuppe, M. A., Merz, S., Feodrippe, P. R., Lamport, L., Schultz, W., Fernandes, A., Ryndzionek, M., Konnov, I., Halterman, J., Wayne, H., and Jobvs. TLA+ CommunityModules. https://github.com/tlaplus/ CommunityModules, 2026. Lamport, L. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems (TOPLAS), May 1994. Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. AddisonWesley, July 2002.

11

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

Lamport, L., Sharma, M., Tuttle, M., and Yu, Y. The Wildfire Challenge Problem. https://www.microsoft. com/en-us/research/wp-content/uploads/ 2016/12/The-Wildfire-Challenge-Problem.pdf, January 2001.

Ouyang, L., Sun, X., Tang, R., Huang, Y., Jivrajani, M., Ma, X., and Xu, T. Multi-Grained Specifications for Distributed System Model Checking and Verification. In Proceedings of the 20th European Conference on Computer Systems (EuroSys), March 2025.

Lattuada, A., Hance, T., Bosamiya, J., Brun, M., Cho, C., LeBlanc, H., Srinivasan, P., Achermann, R., Chajed, T., Hawblitzel, C., Howell, J., Lorch, J. R., Padon, O., and Parno, B. Verus: A Practical Foundation for Systems Verification. In Proceedings of the 30th ACM Symposium on Operating Systems Principles (SOSP), November 2024.

Paulson, L. C. Isabelle: A Generic Theorem Prover. Springer, July 1994.

Lin, X., Cao, Q., Huang, Y., Wang, H., Lu, J., Liu, Z., Song, L., and Liang, X. FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. In Advances in Neural Information Processing Systems (NeurIPS), December 2024. Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M. R. H., Amin, N., and Tegmark, M. DafnyBench: A Benchmark for Formal Software Verification. arXiv:2406.08467, June 2024. Lucas, K., Lynch, A., Tong, L., Champine, L., Straznickas, Z., Distefano, D., Agrawal, H., Ben Asher, E., Howell, A., Jawhar, S., Rohlf, C., Zeldovich, N., Carlini, N., Agrawal, R., and Gross, J. LLMs are making formal software verification feasible at a much larger scale. https://www.anthropic.com/ research/formal-verification, October 2026. Ma, H., Goel, A., Jeannin, J.-B., Kapritsos, M., Kasikci, B., and Sakallah, K. A. I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), October 2019. Mishra, S., Gonçalves, J., Tankuranand, C., Crooks, N., Giridharan, N., Howard, H., and Jensen, C. Pirateship: Append-Only Ledgers for (Mostly) Trusted Execution Environments. In Proceedings of the ACM SIGOPS 32nd Symposium on Operating Systems Principles (SOSP), September 2026. Mugnier, E., Gonzalez, E. A., Polikarpova, N., Jhala, R., and Zhou, Y. Laurel: Unblocking Automated Verification with Large Language Models. Proceedings of the ACM on Programming Languages (PACMPL), April 2025.

Pı̂rlea, G., Gladshtein, V., Kinsbruner, E., Zhao, Q., and Sergey, I. Veil: A Framework for Automated and Interactive Verification of Transition Systems. In Proceedings of the 37th International Conference on Computer Aided Verification (CAV), July 2025. Pnueli, A. The Temporal Logic of Programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), October 1977. Schultz, W. and Demirbas, M. Design and Modular Verification of Distributed Transactions in MongoDB. Proceedings of the VLDB Endowment (PVLDB), August 2025. Song, Y. J. and Renesse, R. Bosco: One-Step Byzantine Asynchronous Consensus. In Proceedings of the 22nd International Symposium on Distributed Computing (DISC), September 2008. Strelbytska, K., Szilágyi, B., Mészáros, A., and Huszár, F. TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents. arXiv:2610.14923, October 2026. Suda, M. and Weidenbach, C. A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), June 2012. Sun, X., Ma, W., Gu, J. T., Ma, Z., Chajed, T., Howell, J., Lattuada, A., Padon, O., Suresh, L., Szekeres, A., and Xu, T. Anvil: Verifying Liveness of Cluster Management Controllers. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2024. Tang, R., Wang, M., Sun, X., Huang, L., Huang, Y., and Ma, X. Converos: Practical Model Checking for Verifying Rust OS Kernel Concurrency. In Proceedings of the 2025 USENIX Annual Technical Conference (ATC), July 2025.

Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., and Deardeuff, M. How Amazon Web Services Uses Formal Methods. Communications of the ACM (CACM), March 2015.

Thompson, K., Saavedra, N., Carrott, P., Fisher, K., SanchezStern, A., Brun, Y., Ferreira, J. F., Lerner, S., and First, E. Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. arXiv:2412.14063, December 2024.

Ongaro, D. and Ousterhout, J. In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Annual Technical Conference (ATC), June 2014.

TLA+ Foundation. Industrial Use of TLA+. https: //foundation.tlapl.us/industry/index.html, 2026.

12

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

TLAi+Bench. TLAi+ Benchmarks on TLA+ Formal Specification Tasks. https://github.com/tlaplus/ TLAiBench, 2026. Xin, Y., Chen, Q., Durrett, G., and Dillig, I. VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean. arXiv:2602.18307, February 2026. Xu, Q., Luan, X., Wang, R., Leang, J., Wang, P., Li, H., Li, W., and Watt, C. Neural Theorem Proving for Verification Conditions: A Real-World Benchmark. In Proceedings of the 14th International Conference on Learning Representations (ICLR), April 2026. Yang, C., Li, X., Misu, M. R. H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J. R., Lu, S., Yang, F., Zhou, Z., and Lu, S. AutoVerus: Automated Proof Generation for Rust Code. Proceedings of the ACM on Programming Languages (PACMPL), October 2025a.

Zhou, Y. and Tripakis, S. Towards Language Model Guided TLA+ Proof Automation. In Proceedings of the 27th International Symposium on Formal Methods (FM), May 2026.

AI U SAGE D ISCLOSURE We used OpenAI Codex with GPT-6 Astra and GPT-6.1 Sol to assist with software development for TLAPS-Bench and its evaluation, as well as paper writing. For software development, we used Codex as the coding agent to help implement TLAPS-Bench and T ILAPIA; we also used Codex to write evaluation scripts. For paper writing, we used Codex to polish the text, including grammar, phrasing, and clarity. All AI-assisted code and text were reviewed by the authors before use. We take full responsibility for the correctness, originality, and integrity of the work.

Yang, C., Neamtu, N., Hawblitzel, C., Lorch, J. R., and Lu, S. VeruSAGE: A Study of Agent-Based Verification for Rust Systems. arXiv:2512.18436, December 2025b. Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., and Ryan, G. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2021. Ye, Z., Lou, H., Sun, Y., Song, P., Yan, Z., Kasriel, T., Zhang, Q., Yang, K., Kong, S., He, J., and Song, D. Vero: Can AI Agents Build Formally Verified Software Repositories? arXiv:2608.13522, August 2026a. Ye, Z., Yan, Z., He, J., Kasriel, T., Yang, K., and Song, D. VERINA: Benchmarking Verifiable Code Generation. In Proceedings of the 14th International Conference on Learning Representations (ICLR), April 2026b. Yu, Y., Manolios, P., and Lamport, L. Model Checking TLA+ Specifications. In Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), September 1999. Zhang, L., Lu, S., and Duan, N. Selene: Pioneering Automated Proof in Software Verification. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (ACL), August 2024. Zhong, S. C. and Si, X. Towards Repository-Level Program Verification with Large Language Models. In Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL), October 2025.

13

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

A

OTHER TLAPS-B ENCH P ROBLEMS

In this paper, our evaluation focused on 12 specifications with 70 proof targets shown in Table 2. In total, TLAPS-Bench includes 95 TLA+ specifications and 265 proof targets. Table A1 shows the remaining problems. Most of the problems in Table A1 are retired after the frontier proved them—they can be used for evaluation, but can no longer challenge frontier models. On the other hand, the proofs of these specifications generated by AI agents are valuable and are shared as public knowledge in our project repository. Table A1. The retired problem set of TLAPS-Bench. Specification

Type

Model Source

Spec LOC

Atomic Bakery Atomic Bakery (without SMT) Bakery Peterson Simple mutex Bakery Boulangerie Lamport mutex Lock LockHS Peterson (auxiliary variables) Two-thread mutex Ticket lock Nested ticket lock Allocator Allocator implementation Scheduling allocator Simple allocator Barriers Readers–writers Cigarette smokers LLVM libomp Blocking queue (fair) Blocking queue (split) Blocking queue Disruptor (MPMC) Disruptor (SPMC) Split queue TLC DiskStateQueue B-tree Key-value store German control German data Paxos: Consensus Paxos Paxos (history variable) Consensus: Consensus Consensus: PaxosProof Consensus: Voting Record Paxos: Consensus Paxos: Voting Paxos lecture: Consensus Paxos lecture: Voting Paxos lecture: Voting proof Tencent Paxos Byzantine Paxos: BPConProof Byzantine Paxos: Consensus Byzantine Paxos: PConProof Byzantine Paxos: VoteProof

Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol System System System Protocol Protocol Protocol Protocol Protocol Protocol Protocol System System System System System System System System System System Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol System Protocol Protocol Protocol Protocol

TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository Anvil Ivy examples Ivy examples TLAPS Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository Specula TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository Ivy examples TLA+ tools TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLAPS Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository

14

106 101 123 76 50 127 141 106 52 190 122 48 70 81 44 186 98 72 215 104 45 596 167 152 67 215 187 74 1,567 313 106 119 283 24 159 105 51 208 128 49 30 83 27 101 78 189 400 36 94 147

Targets 1 (Safety) 1 (Safety) 1 (Safety) 2 (Safety + Liveness) 2 (Safety) 2 (Safety) 2 (Safety) 2 (Safety) 1 (Safety) 2 (Safety + Refinement) 2 (Safety + Refinement) 1 (Liveness) 2 (Safety + Liveness) 2 (Safety + Liveness) 4 (Safety) 1 (Safety) 2 (Safety) 2 (Safety) 5 (Safety + Refinement) 2 (Safety) 2 (Safety) 4 (Safety) 1 (Refinement) 3 (Safety + Refinement) 1 (Safety) 2 (Safety) 2 (Safety) 1 (Liveness) 1 (Safety) 5 (Safety) 1 (Safety) 1 (Safety) 6 (Safety + Refinement) 1 (Safety) 3 (Safety + Refinement) 2 (Safety) 1 (Safety) 3 (Safety + Refinement) 6 (Safety + Refinement) 1 (Refinement) 2 (Safety + Liveness) 2 (Safety + Refinement) 1 (Safety) 2 (Safety + Refinement) 3 (Safety) 2 (Safety) 3 (Safety + Refinement) 3 (Safety + Liveness) 1 (Safety) 4 (Safety + Liveness + Refinement)

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System Table A1 (continued) Specification Byzantine reliable broadcast Bosco Byzantine consensus Sailfish BFT consensus Nano blockchain Hybrid reliable broadcast Two-phase handshake Two-phase handshake (proof) Paxos commit Transaction commit Two-phase commit Walgit WAL SlateDB WAL OSWALD WAL BufferedRandomAccessFile EWD840 termination detection EWD840 EWD840: synchronous detection Dijkstra–Scholten (EWD687a) EWD998: asynchronous detection EWD998 (PlusCal) EWD998 Termination detection Misra reachability (parallel) Misra reachability (sequential) Spanning tree (SpanTree) Spanning tree (spanning) TCP Alternating-bit protocol FiniteMonotonic CRDT Multi-car elevator Voucher lifecycle PCR workflows: clean PCR workflows: stages

Type Protocol Protocol Protocol System Protocol Protocol Protocol Protocol Protocol Protocol System System System System Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol System Protocol Protocol

Model Source

Spec LOC

+

TLA Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository Ivy examples TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository s3-wal-collection s3-wal-collection s3-wal-collection TLA+ Specification Repository TLAPS Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository Ivy examples TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository TLA+ Specification Repository

Total

130 140 200 390 224 51 50 185 46 112 558 546 260 334 73 121 57 132 71 172 191 69 143 76 48 44 264 132 66 226 66 68 106

Targets 5 (Safety) 5 (Safety) 3 (Safety) 1 (Safety) 3 (Safety + Liveness) 1 (Refinement) 1 (Refinement) 1 (Safety) 1 (Safety) 2 (Safety) 7 (Safety) 4 (Safety) 3 (Safety) 14 (Safety + Refinement) 1 (Safety) 2 (Safety + Refinement) 3 (Safety + Liveness) 3 (Safety) 3 (Safety + Liveness) 2 (Safety + Refinement) 2 (Safety + Refinement) 1 (Safety) 1 (Refinement) 1 (Safety) 1 (Safety) 1 (Safety) 3 (Safety) 2 (Safety + Liveness) 3 (Safety + Liveness) 2 (Safety) 1 (Safety) 2 (Safety) 1 (Safety) 195

15

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

B

D ETAILED B ENCHMARK R ESULTS

Table A2 shows the proof results for each target and model configuration. Tables A3–A14 report pass@3 success rates and total resource usage across all three runs. 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. Target

Kind

FLASH cache coherence protocol TypeOK ReqProgress DirProgress UniProgress InvProgress RpProgress WbProgress ShWbProgress NakcProgress CacheDataProp MemDataProp ExCopyProp FwdGetPending FwdGetXPending InvalidationAckProp

S L L L L L L L L S S S S S S

ZooKeeper protocol (Zab) Leadership1 Leadership2 PrefixConsistency Integrity Agreement TotalOrder LocalPrimaryOrder GlobalPrimaryOrder PrimaryIntegrity

S S S S S S S S S

GPT-6.1 Sol

GPT-6 Astra

GPT-5.6 Terra high

low

GPT-6 Luna

max

high

low

max

high

low

max

max

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

✓

✓

✓ ✓ ✓ ✓ ✓

✓ ✓ ✓

✓ ✓ ✓ ✓ ✓

✓

Cahill’s serializable snapshot isolation protocol CahillSerializable S Ivy TLB NoError NonStarvation

S L

✓

✓

✓

✓

✓

✓

✓

✓

OpenAddressing CompleteAsSafety Consistent Contains Duplicates Sorted

S S S S S

✓ ✓ ✓ ✓ ✓

✓

✓

✓

✓

✓

✓

✓

✓

✓

✓

✓

✓

✓

✓

etcd Raft LogInv CommittedIsDurableInv LeaderTermMaxIndexInv LeaderCompletenessInv LogMatchingInv LeaderUniqueness MoreUpToDateCorrectInv QuorumLogInv

S S S S S S S S

✓

✓

✓

✓

✓

HashiCorp Raft LeaderCompleteness StateMachineSafety CommittedEntriesPreserved

S S S

✓ ✓ ✓

16

high

low

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System Table A2 (continued) Target

Kind

LogMatching ElectionSafety ConfigurationSafety

S S S

ZooKeeper implementation Leadership1 Leadership2 PrefixConsistency Integrity Agreement TotalOrder LocalPrimaryOrder GlobalPrimaryOrder PrimaryIntegrity

S S S S S S S S S

MongoDB distributed transactions SnapshotIsolation

S

CCF CommittedLogsAgree CommittedLogsAppendOnly

S S

PirateShip TypeOK IndexBoundsInv BranchInv AuditBranchInv OneLeaderPerViewInv WellFormedBranchInv ViewMonotonicInv ViewStabilizationInv CommittedBranchAppendOnlyProp AuditedBranchAppendOnlyProp MonotonicAuditedIndexProp

S S S S S S S S S S S

Wildfire Refinement

R

Accepted targets

GPT-6.1 Sol

GPT-6 Astra

GPT-5.6 Terra

max

high

low

max

high

low

max

✓

✓

✓

✓

✓

✓

✓

GPT-6 Luna

high

low

max

high

low

0

0

7

0

0

✓ ✓

✓

✓

✓

✓

✓

✓

✓

✓ ✓

✓ ✓

✓

✓

✓

✓ ✓

✓ ✓

✓ ✓

✓ ✓ ✓ ✓

✓

✓

✓

✓

✓

✓

31

24

25

30

24

24

15

Model

Effort

Table A3. Results for the FLASH cache coherence protocol. Success Rate Total Tokens (M) Total Cost (pass@3) Input Output (USD)

GPT-6.1 Sol

max high low

100.0% (15/15) 100.0% (15/15) 100.0% (15/15)

161.15 119.17 209.83

0.702 0.509 0.798

37.27 24.92 36.96

510.7 338.1 665.6

GPT-6 Astra

max high low

100.0% (15/15) 100.0% (15/15) 100.0% (15/15)

129.77 114.09 125.19

0.557 0.426 0.395

172.75 146.29 158.78

755.3 419.5 429.9

GPT-5.6 Terra

max high low

73.3% (11/15) 0.0% (0/15) 0.0% (0/15)

2054.57 12.89 3.96

6.003 0.062 0.021

555.88 4.34 1.49

4890.6 50.5 21.0

GPT-6 Luna

max high low

26.7% (4/15) 0.0% (0/15) 0.0% (0/15)

194.40 5.43 1.14

0.861 0.036 0.005

2.64 0.09 0.03

359.5 17.9 2.8

17

Total Agent Time (min)

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

Table A4. Results for the ZooKeeper protocol (Zab). Success Rate Total Tokens (M) Total Cost (pass@3) Input Output (USD)

Total Agent Time

Model

Effort

GPT-6.1 Sol

max high low

0.0% (0/9) 0.0% (0/9) 0.0% (0/9)

13.05 15.49 14.65

0.160 0.140 0.089

3.66 3.83 3.04

77.5 94.9 53.3

GPT-6 Astra

max high low

11.1% (1/9) 0.0% (0/9) 0.0% (0/9)

43.04 10.50 9.21

0.380 0.082 0.056

71.11 17.44 14.40

237.2 54.4 42.7

GPT-5.6 Terra

max high low

0.0% (0/9) 0.0% (0/9) 0.0% (0/9)

2220.78 9.53 2.64

6.001 0.046 0.018

580.62 3.20 1.16

4415 35.1 17.9

GPT-6 Luna

max high low

0.0% (0/9) 0.0% (0/9) 0.0% (0/9)

105.81 4.19 1.44

0.514 0.023 0.005

1.44 0.07 0.03

164.6 31.9 4.1

Model

Table A5. Results for Cahill’s serializable snapshot isolation protocol. Success Rate Total Tokens (M) Total Cost Effort (pass@3) Input Output (USD)

Total Agent Time

GPT-6.1 Sol

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

36.71 19.41 2.40

0.296 0.136 0.023

8.01 4.32 0.81

172.4 82.3 14.1

GPT-6 Astra

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

18.60 8.03 1.90

0.146 0.057 0.017

31.53 13.28 4.18

77.6 39.0 13.5

GPT-5.6 Terra

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

2548.60 6.93 3.21

5.996 0.048 0.019

644.28 2.57 1.29

6256.9 40.4 25.1

GPT-6 Luna

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

23.30 1.57 0.61

0.183 0.018 0.003

0.37 0.04 0.02

65.6 8.3 3.0

Total Cost

Total Agent Time

(USD)

(min)

(min)

(min)

Model

Effort

Table A6. Results for Ivy TLB. Success Rate Total Tokens (M) (pass@3) Input Output

GPT-6.1 Sol

max high low

50.0% (1/2) 50.0% (1/2) 50.0% (1/2)

61.77 62.02 45.09

0.407 0.275 0.210

11.98 10.25 8.26

216.3 175.3 168.8

GPT-6 Astra

max high low

50.0% (1/2) 50.0% (1/2) 50.0% (1/2)

43.32 20.14 25.64

0.238 0.116 0.125

60.84 29.84 35.53

139.7 93.4 103.6

GPT-5.6 Terra

max high low

50.0% (1/2) 0.0% (0/2) 0.0% (0/2)

1922.13 16.65 4.53

6.002 0.074 0.033

515.81 5.13 1.73

3097.6 54.3 29.9

GPT-6 Luna

max high low

50.0% (1/2) 0.0% (0/2) 0.0% (0/2)

995.78 1.86 1.69

3.649 0.019 0.008

13.03 0.04 0.04

2475.9 18.3 4.1

18

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

Model

Effort

Table A7. Results for OpenAddressing. Success Rate Total Tokens (M) (pass@3) Input Output

GPT-6.1 Sol

max high low

100.0% (5/5) 40.0% (2/5) 40.0% (2/5)

275.38 30.05 17.45

GPT-6 Astra

max high low

40.0% (2/5) 40.0% (2/5) 40.0% (2/5)

GPT-5.6 Terra

max high low

GPT-6 Luna

Total Cost

Total Agent Time

(USD)

(min)

1.194 0.168 0.085

56.93 6.01 3.33

846.1 93.6 44.0

40.27 18.52 19.32

0.241 0.102 0.069

59.60 27.16 26.00

150.0 61.5 53.6

40.0% (2/5) 0.0% (0/5) 0.0% (0/5)

2266.44 10.95 2.85

6.005 0.060 0.020

594.60 3.62 1.21

6356.0 32.1 15.3

max high low

40.0% (2/5) 0.0% (0/5) 0.0% (0/5)

702.70 4.96 0.55

2.682 0.040 0.005

9.13 0.10 0.01

1452.2 37.6 1.4

Model

Effort

Table A8. Results for etcd Raft. Success Rate Total Tokens (M) (pass@3) Input Output

Total Cost

Total Agent Time

(USD)

(min)

GPT-6.1 Sol

max high low

37.5% (3/8) 12.5% (1/8) 12.5% (1/8)

189.90 63.50 57.87

0.696 0.272 0.286

38.60 10.59 9.89

479.1 265.2 199.5

GPT-6 Astra

max high low

12.5% (1/8) 12.5% (1/8) 12.5% (1/8)

47.60 47.67 27.31

0.241 0.179 0.199

66.92 61.27 41.52

220.8 171.3 253.4

GPT-5.6 Terra

max high low

0.0% (0/8) 0.0% (0/8) 0.0% (0/8)

2998.18 5.44 2.85

6.006 0.042 0.020

750.54 2.09 1.26

9107.1 28.3 18.2

GPT-6 Luna

max high low

0.0% (0/8) 0.0% (0/8) 0.0% (0/8)

18.80 1.52 0.75

0.190 0.019 0.005

0.33 0.04 0.02

65.1 7.0 2.0

Total Cost

Total Agent Time

(USD)

(min)

Model

Effort

Table A9. Results for HashiCorp Raft. Success Rate Total Tokens (M) (pass@3) Input Output

GPT-6.1 Sol

max high low

16.7% (1/6) 16.7% (1/6) 16.7% (1/6)

29.26 17.87 48.53

0.259 0.121 0.195

6.74 3.81 8.04

157.9 66.7 164.6

GPT-6 Astra

max high low

16.7% (1/6) 16.7% (1/6) 16.7% (1/6)

17.10 20.32 18.44

0.135 0.110 0.095

28.00 29.47 26.59

82.0 73.3 76.4

GPT-5.6 Terra

max high low

16.7% (1/6) 0.0% (0/6) 0.0% (0/6)

1822.03 9.53 2.97

4.606 0.046 0.020

476.72 3.20 1.24

4625.9 40.6 20.7

GPT-6 Luna

max high low

0.0% (0/6) 0.0% (0/6) 0.0% (0/6)

69.40 1.66 0.76

0.384 0.019 0.004

0.98 0.04 0.02

111.4 14.8 1.8

19

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

Table A10. Results for the ZooKeeper implementation. Success Rate Total Tokens (M) Total Cost (pass@3) Input Output (USD)

Total Agent Time

Model

Effort

GPT-6.1 Sol

max high low

0.0% (0/9) 0.0% (0/9) 0.0% (0/9)

33.22 23.43 10.27

0.266 0.205 0.060

7.58 5.57 2.20

131.3 195.6 41.6

GPT-6 Astra

max high low

22.2% (2/9) 0.0% (0/9) 0.0% (0/9)

122.50 17.48 5.43

0.367 0.097 0.028

145.98 25.32 8.92

229.3 78.9 21.2

GPT-5.6 Terra

max high low

0.0% (0/9) 0.0% (0/9) 0.0% (0/9)

2255.79 15.98 2.05

6.002 0.052 0.016

587.39 4.82 0.98

5290.9 56.1 14.8

GPT-6 Luna

max high low

0.0% (0/9) 0.0% (0/9) 0.0% (0/9)

23.73 3.25 1.06

0.151 0.019 0.005

0.36 0.06 0.02

54.1 12.4 2.6

Table A11. Results for MongoDB distributed transactions. Success Rate Total Tokens (M) Total Cost (pass@3) Input Output (USD)

Total Agent Time

(min)

Model

Effort

GPT-6.1 Sol

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

23.33 11.50 9.95

0.183 0.071 0.057

5.42 2.48 2.06

109.8 42.2 29.9

GPT-6 Astra

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

15.36 6.88 4.81

0.111 0.051 0.025

24.49 11.84 7.79

76.2 32.2 17.9

GPT-5.6 Terra

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

761.25 11.86 1.93

2.530 0.058 0.016

207.59 3.82 0.90

2349.4 52.6 10.3

GPT-6 Luna

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

31.62 2.27 0.70

0.275 0.021 0.006

0.53 0.05 0.02

74.1 10.0 1.9

Model

Effort

Success Rate (pass@3)

GPT-6.1 Sol

max high low

GPT-6 Astra

Table A12. Results for CCF. Total Tokens (M)

(min)

Total Cost

Total Agent Time

Input

Output

(USD)

(min)

50.0% (1/2) 0.0% (0/2) 0.0% (0/2)

513.56 200.27 14.68

2.677 1.062 0.065

123.55 49.85 2.62

2620.9 1029.7 58.0

max high low

50.0% (1/2) 0.0% (0/2) 0.0% (0/2)

151.45 27.13 9.24

1.054 0.118 0.031

226.18 37.51 12.74

1041.4 114.2 138.2

GPT-5.6 Terra

max high low

0.0% (0/2) 0.0% (0/2) 0.0% (0/2)

1632.57 11.93 3.78

4.309 0.054 0.023

423.87 3.81 1.46

3353.0 44.2 16.4

GPT-6 Luna

max high low

0.0% (0/2) 0.0% (0/2) 0.0% (0/2)

40.41 2.53 2.51

0.207 0.021 0.010

0.56 0.06 0.04

110.2 11.0 5.7

20

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

Model

Effort

Table A13. Results for PirateShip. Success Rate Total Tokens (M) (pass@3) Input Output

GPT-6.1 Sol

max high low

45.5% (5/11) 36.4% (4/11) 45.5% (5/11)

108.28 63.56 115.43

GPT-6 Astra

max high low

54.5% (6/11) 36.4% (4/11) 36.4% (4/11)

GPT-5.6 Terra

max high low

GPT-6 Luna

Total Cost

Total Agent Time

(USD)

(min)

0.788 0.289 0.350

26.35 11.00 19.73

538.5 299.2 342.1

131.92 55.19 22.32

0.716 0.274 0.101

182.73 75.18 30.58

918.1 303.5 84.1

0.0% (0/11) 0.0% (0/11) 0.0% (0/11)

932.62 9.19 3.26

2.422 0.045 0.024

246.21 3.05 1.29

2495.3 55.2 18.2

max high low

0.0% (0/11) 0.0% (0/11) 0.0% (0/11)

127.58 3.35 1.74

0.403 0.032 0.010

1.64 0.07 0.03

336.5 26.3 14.9

Model

Effort

Table A14. Results for Wildfire. Success Rate Total Tokens (M) (pass@3) Input Output

Total Cost

Total Agent Time

(USD)

(min)

GPT-6.1 Sol

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

10.53 9.29 3.08

0.103 0.064 0.021

2.78 2.13 0.82

56.9 42.3 14.3

GPT-6 Astra

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

9.29 7.15 4.05

0.083 0.050 0.019

16.31 11.96 6.38

65.0 134.4 27.9

GPT-5.6 Terra

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

60.91 5.96 1.43

0.352 0.048 0.014

18.65 2.35 0.77

243.8 39.2 7.1

GPT-6 Luna

max high low

0.0% (0/1) 0.0% (0/1) 0.0% (0/1)

4.63 1.38 0.85

0.087 0.016 0.003

0.11 0.03 0.02

16.2 4.7 1.5

21

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

C

ACCEPTED P ROOFS , I NCOMPLETE P ROOFS , AND D ISPROVED TARGETS

This appendix shows simplified versions of proofs submitted by agents in the benchmark runs of Section 5, including both accepted proofs and incomplete proofs. We also include one disproved target found during task validation (Section 4.3). In TLAPS, a BY clause lists facts and proof hints to justify a proof step. A hint can choose a backend prover or pick a proof strategy: SMTT calls an SMT solver, Isa calls Isabelle, PTL calls the temporal logic prover, ExpandENABLED hints the backend to expand the ENABLED operator. We drop some auxiliary steps to keep the examples short. C.1

Accepted Proofs

FLASH: eventual message delivery. FLASH has eight liveness targets concerning request completion and message delivery. Example 1 shows a proof of WbProgressCorrect, which states that a pending writeback message is eventually delivered under the assumption of weak fairness: if the action remains enabled, it eventually takes a step (Lamport, 1994). The action NI Wb delivers the message, and the specification FairSpec assumes weak fairness of NI Wb. Step <1>1 shows that NI Wb can be taken while the message is pending, using the type invariant TypeOK. Step <1>2 shows that if NI Wb is taken, the message will be delivered. Step <1>3 extracts the fairness assumption from FairSpec, and step <1>4 shows that TypeOK always holds by reusing the proved target TypeCorrect. The other seven liveness targets follow the same pattern or chain several such steps through helper lemmas. \* (target and action, from the read-only task files) WbProgress == (WbMsg.Cmd = "WB_Wb") ∼> (WbMsg.Cmd = "WB_None") NI_Wb == /\ WbMsg.Cmd = "WB_Wb" /\ WbMsg' = [Cmd |-> "WB_None", Proc |-> Undefined, Data |-> Undefined] /\ ... \* (omitted: directory and memory updates) THEOREM WbProgressCorrect == FairSpec => WbProgress <1>1. TypeOK /\ (WbMsg.Cmd # "WB_None") => ENABLED <<NI_Wb>>_vars BY SMTT("r30"), ExpandENABLED DEF NI_Wb, TypeOK, vars, pendVars, fwdVars, RP_CMD, WB_CMD, SHWB_CMD, NAKC_CMD <1>2. <<NI_Wb>>_vars => (WbMsg.Cmd = "WB_None")' BY SMTT("r10") DEF NI_Wb, vars <1>3. FairSpec => WF_vars(NI_Wb) BY Isa DEF FairSpec, Fairness <1>4. FairSpec => []TypeOK BY TypeCorrect, SMTT("r10") DEF FairSpec, Spec <1>5. QED BY <1>1, <1>2, <1>3, <1>4, PTL DEF WbProgress Example 1. Accepted proof of the FLASH liveness target by GPT-6.1 Sol at high effort (simplified).

etcd Raft: leader uniqueness. The target LeaderUniqueness states that two leaders in the same term are the same server. Example 2 shows the accepted proof by GPT-6 Astra at max effort, and Figure 2 shows a simplified version of this task. The auxiliary invariant AgElectionInv treats each granted vote as a ballot <<voter, term, candidate>>, wherever the vote is currently stored: in a pending or delivered vote response, or in the votesGranted set of a candidate or leader. AgAgreement states that a voter’s ballots in one term name at most one candidate. AgPendingBound and AgDurableBound tie each ballot to the voter’s own term and vote. They use durable state for delivered and collected votes, so the invariant still holds after a server crashes and restarts. Given the invariant, the target follows from quorum intersection: two leaders in the same term each hold a quorum of votes, a voter in both quorums has a ballot for each leader, and AgAgreement makes the two leaders equal. The agent proves that every action preserves the invariant with one lemma per action. \* Vote certificates are retained in pending messages, delivered messages, \* and the vote sets of active candidates and leaders. AgVoteMsgs(bag) == {m \in DOMAIN bag : m.mtype = RequestVoteResponse /\ m.mvoteGranted} AgMsgBallots(bag) == {<<m.msource, m.mterm, m.mdest>> : m \in AgVoteMsgs(bag)} AgPending == AgMsgBallots(pendingMessages) AgSent == AgMsgBallots(messages)

22

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System AgGranted == UNION {{<<v, currentTerm[i], i>> : v \in votesGranted[i]} : i \in {j \in Server : AgActive(j)}} AgBallots == AgPending \cup AgSent \cup AgGranted \* Pending votes are protected by volatile state. Delivered and collected \* votes are protected by durable state, so their protection survives a crash. AgPendingBound == \A b \in AgPending : /\ b[2] <= currentTerm[b[1]] /\ b[2] = currentTerm[b[1]] => votedFor[b[1]] = b[3] AgDurableBound == \A b \in AgSent \cup AgGranted : /\ b[2] <= durableState[b[1]].currentTerm /\ b[2] = durableState[b[1]].currentTerm => durableState[b[1]].votedFor = b[3] \* A voter has at most one candidate among certificates for the same term. AgAgreement == \A b, c \in AgBallots : b[1] = c[1] /\ b[2] = c[2] => b[3] = c[3] AgElectionInv == /\ AgBasic /\ ... \* (AgBasic includes state[i] = Leader => \* votesGranted[i] \in Quorum(InitServer)) /\ AgPendingBound /\ AgDurableBound /\ AgAgreement LEMMA AgElectionSafetyConsequence == AgElectionInv => LeaderUniqueness <1>1. ASSUME AgElectionInv, NEW i \in Server, NEW j \in Server, currentTerm[i] = currentTerm[j], state[i] = Leader, state[j] = Leader PROVE i = j <2>1. votesGranted[i] \in Quorum(InitServer) /\ votesGranted[j] \in Quorum(InitServer) BY <1>1, SMTT("r5") DEF AgElectionInv, AgBasic <2>2. PICK v \in InitServer : v \in votesGranted[i] /\ v \in votesGranted[j] BY <2>1, AgQuorumIntersection, FiniteServers <2>3. <<v, currentTerm[i], i>> \in AgBallots /\ <<v, currentTerm[j], j>> \in AgBallots BY <1>1, <2>2, SMTT("r5") DEF AgBallots, AgGranted, AgActive <2>4. QED BY <1>1, <2>3, SMTT("r5") DEF AgElectionInv, AgAgreement <1>2. QED BY <1>1 DEF LeaderUniqueness \* (omitted: AgElectionInit and AgElectionStep, the initial-state and step lemmas) LEMMA AgElectionAlways == Spec => []AgElectionInv BY AgElectionInit, AgElectionStep, PTL DEF Spec THEOREM LeaderUniquenessTheorem == Spec => []LeaderUniqueness BY ONLY AgElectionAlways, AgElectionSafetyConsequence, PTL Example 2. Accepted proof of the etcd Raft target LeaderUniqueness by GPT-6 Astra at max effort (simplified).

C.2

Proof Failures

An accepted proof of a safety target Spec => []P (Example 2) usually requires discovering and proving auxiliary invariants and helper lemmas, and deriving P from these proof facts. Liveness targets (Example 1) additionally require progress lemmas connecting fairness assumptions with intermediate state machine stages. Any missing segment in the proof chain will fail the task. The two most common failure categories in Table 5 are undecomposed proof attempts and incomplete proofs. In undecomposed attempts, agents submit entire targets directly to backends. Agents may do so before developing a proof strategy or after their own proof attempts stall. We illustrate this with an Ivy TLB example below. Incomplete proofs reveal difficulties in discovering useful invariants, establishing proposed invariants or lemmas, and connecting established results to the target property. We present one example for each of these three cases below. Undecomposed liveness proof: Ivy TLB. GPT-6 Astra at max effort proved the TLB safety target with an inductive invariant AGInv, and all 30 of its helper lemmas passed verification. For the liveness target NonStarvation, however, the agent submitted a single call to the temporal-logic backend PTL (Example 3), which must derive the target from the definitions of Spec and NonStarvation alone. A liveness proof instead needs progress lemmas showing that, under the

23

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

fairness assumptions in Spec, the processor’s loops terminate and the locks it waits for are eventually released. The agent did attempt such a proof in scratch modules alongside the safety proof, and checked its finiteness and control-flow steps. However, it could not prove that the actions in the fairness assumptions are enabled, which is required to apply fairness. It kept these attempts out of the submission and ended the session with the one-step proof it had written at the start, which the backend rejects in under a second. \* (target and fairness assumptions, from the read-only task files) Spec == /\ SafetySpec \* (Init /\ [][Next]_vars) /\ \A p \in Processor : WF_vars(Step(p)) /\ \A p \in Processor : SF_vars(BootStep(p)) /\ \A p \in Processor : SF_vars(AcquirePmapLock(p)) /\ \A p \in Processor : SF_vars(AcquireResponderActionLock(p)) ProcessorMakesProgress(p) == pc[p] \in {MainCheck, ResponderClearActionNeeded} NonStarvation == \A p \in Processor : TRUE ∼> ProcessorMakesProgress(p) \* (helpers for Safety, all verified; proofs and the per-action lemmas omitted) AGInv == AGType /\ AGPmap /\ AGAction /\ AGControl /\ AGCoverage /\ AGCoherent /\ ∼error LEMMA AGInitial == Init => AGInv LEMMA AGInduction == AGInv /\ [Next]_vars => AGInv' LEMMA AGInvariant == SafetySpec => []AGInv THEOREM Safety == SafetySpec => []NoError BY AGInvariant, PTL DEF AGInv, NoError THEOREM Liveness == Spec => NonStarvation BY PTL DEF Spec, NonStarvation Example 3. Undecomposed proof of the Ivy TLB liveness target NonStarvation by GPT-6 Astra at max effort (simplified). Safety is accepted; the one-step proof of Liveness fails verification.

Missing invariant for one case: OpenAddressing. In the OpenAddressing model, writers insert fingerprints into a hash table. A writer probes up to L slots, starting from the fingerprint’s home slot idx(f, 0). If it finds neither the fingerprint nor a free slot, it triggers an eviction, which moves table entries into external sorted sequences. GPT-6 Astra at max effort proves two of the five targets and verifies all 50 of its helper lemmas, but leaves Consistent (Example 4) and other proofs incomplete. The proof splits into two cases. In the first case, OAHashScale > 0 and L > 0, so distinct fingerprints have distinct home slots, every insertion succeeds at its first probe, and no eviction occurs. The invariant OADirectInv describes this behavior, and this case is verified. The second case covers hash collisions and evictions, where probing and eviction actually take place. The agent’s comment notes that this case needs a stronger invariant, but the step cites only three existing invariants, and the SMT solver fails to prove it. The proof therefore covers only configurations without collisions or evictions. \* (when OAHashScale > 0, distinct fingerprints have distinct home slots idx(f, 0)) OAHashScale == (K-1) \div (max(fps)-min(fps)) OADirectInv == /\ ... \* (omitted: types and control states) /\ external = <<>> /\ newexternal = <<>> /\ evict = FALSE /\ index = [w \in Writer |-> 0] /\ \A i \in 1..K : table[i] # empty => i = idx(table[i],0) /\ ... THEOREM Spec => []Consistent <1>1. OAHashScale > 0 /\ L > 0 => (Spec => []Consistent) <2>1. OADirectInv => Consistent BY OADirectSafety <2>2. QED BY <2>1, OADirectInvariant, PTL <1>2. OAHashScale = 0 \/ L = 0 => (Spec => []Consistent)

24

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System \* The collision case also needs preservation of the table and scan invariant. BY OAControlInvariant, OATypesInvariant, OASortedInvariant, SMTT("r1") <1>3. OAHashScale \in Nat /\ L \in Nat BY OAHashScaleType, OAAssumption, SMTT("r10") <1>4. QED BY <1>1, <1>2, <1>3, SMTT("r10") Example 4. Incomplete proof of the OpenAddressing target Consistent by GPT-6 Astra at max effort (simplified). Step <1>2 fails verification.

Missing progress lemmas: Ivy TLB. GPT-6 Astra at high effort proved the TLB safety target with an inductive invariant and verified all 29 of its helper lemmas. Its proof of the liveness target NonStarvation (Example 5) combined this invariant and the specification’s fairness assumptions and tried to prove the liveness goal. However, the agent did not state the progress lemmas needed to show that the locks are eventually released and the processor’s loops terminate. As a result, the final step failed verification, and a comment the agent left in the proof listed these missing steps. \* (target and fairness assumptions, from the read-only task files) Spec == /\ SafetySpec \* (Init /\ [][Next]_vars) /\ \A p \in Processor : WF_vars(Step(p)) /\ \A p \in Processor : SF_vars(BootStep(p)) /\ \A p \in Processor : SF_vars(AcquirePmapLock(p)) /\ \A p \in Processor : SF_vars(AcquireResponderActionLock(p)) ProcessorMakesProgress(p) == pc[p] \in {MainCheck, ResponderClearActionNeeded} NonStarvation == \A p \in Processor : TRUE ∼> ProcessorMakesProgress(p) \* (helpers, all verified; proofs and most conjuncts omitted) AgentInv == AgentTypes /\ AgentActivity /\ AgentPmapLock /\ ... /\ NoError LEMMA AgentInitial == Init => AgentInv LEMMA AgentInductive == AgentInv /\ [Next]_vars => AgentInv' THEOREM Liveness == Spec => NonStarvation <1>1. SafetySpec => []AgentInv BY AgentInitial, AgentInductive, PTL DEF SafetySpec <1>2. ASSUME NEW p \in Processor PROVE Spec => (TRUE ∼> ProcessorMakesProgress(p)) <2>1. Spec => []AgentInv BY <1>1 DEF Spec <2>2. Spec => WF_vars(Step(p)) BY <1>2 DEF Spec <2>3. Spec => /\ SF_vars(BootStep(p)) /\ SF_vars(AcquirePmapLock(p)) /\ SF_vars(AcquireResponderActionLock(p)) BY <1>2 DEF Spec \* Remaining obligation: termination of the two todo loops and \* eventual release of the locks on which this processor can wait. <2> QED BY <2>1, <2>2, <2>3, PTL DEF ProcessorMakesProgress <1> QED BY <1>2 DEF NonStarvation Example 5. Incomplete proof of the Ivy TLB liveness target NonStarvation by GPT-6 Astra at high effort (simplified). Step <2> QED fails verification, as do steps <2>1–<2>3.

Unproved invariant: Cahill SSI. GPT-6 Astra at max effort stated a candidate invariant CSInvariant for SSI and proved that it implies serializability and holds at Init (step <1>1 of Example 6), but it did not prove the inductive step <1>2, which shows that every action preserves the invariant. Instead, the agent tested the invariant with TLC by simulating executions from Init. Passing these tests only shows that CSInvariant holds in the sampled reachable states of a small model, while the proof additionally requires it to be inductive. CSInvariant == /\ CSStateTypes /\ CSCore /\ CSWaitSafe /\ CSHistoryConditions(history, inConflict, outConflict)

25

TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System \* (helpers, both verified; proofs omitted) LEMMA CSInvariantInitial == Init => CSInvariant LEMMA CSInvariantSafety == CSInvariant => CahillSerializable(history) THEOREM CahillSerializableCorrect == Spec => []CahillSerializable(history) <1>1. Init => CSInvariant BY CSInvariantInitial, SMTT("r5") <1>2. CSInvariant /\ Next => CSInvariant' BY SMTT("r5") DEF CSInvariant, Next <1>3. CSInvariant /\ UNCHANGED allvars => CSInvariant' ... \* (omitted: proof for stuttering steps) <1>4. CSInvariant => CahillSerializable(history) BY CSInvariantSafety, SMTT("r5") <1>5. QED BY <1>1, <1>2, <1>3, <1>4, PTL DEF Spec \* (the agent's TLC model, scratch/MCCahill.tla and MCCahill.cfg) MCInv == CSInvariant /\ CahillSerializable(history) INIT Init NEXT Next INVARIANT MCInv Example 6. Incomplete proof of the Cahill SSI target by GPT-6 Astra at max effort (simplified), with the TLC model it used to test the invariant. Step <1>2 fails verification. The TLC model starts from Init, so it checks the invariant only on reachable states.

C.3

Disproved Targets

SlateDB WAL: a counterexample to the target. A task can also end with a counterexample when the target is false (Section 4.1). In a run before the evaluation of Section 5, GPT-6 Astra at max effort proved one of the four targets of the original SlateDB WAL model and reported that ConsistentMachineData does not hold and submitted a 58-transition TLC counterexample. Example 7 shows the agent’s summary of the trace. We reproduced the trace, reported it upstream, and revised the model; Appendix D describes the repair, after which Astra proves all four targets. The essential schedule is: 1. Writer w1 becomes ready with a fence at WAL ID 1. 2. Writer w2 chooses WAL ID 2 as its fence position. Before it claims its epoch, w1 appends v1 at ID 2 and v2 at ID 3. 3. w2 claims epoch 2 and passes the boundary check, but delays writing its fence. 4. w3 claims epoch 3, writes its fence at ID 4, validates successfully, and starts replaying. Pause it before replaying ID 2. 5. w4 claims epoch 4, writes its fence at ID 5, replays the full log, and commits snapshot 5 containing <<v1, v2>>. The latest manifest now has ID 6 and replayAfterWalId = 6. 6. The garbage collector deletes the data entry at ID 2, leaving ID 3 present. 7. The delayed w2 writes a fence at the now-vacant ID 2. 8. w3 skips the new fence at ID 2, reads v2 at ID 3, skips its own fence at ID 4, and reaches READY with machine data <<v2>>. The final history is <<[walId |-> 2, value |-> v1], [walId |-> 3, value |-> v2]>>. Since v1 # v2, PrefixOf(<<v2>>, auxWrittenEntries) is false. Thus Spec => []ConsistentMachineData is false under the supplied context. Example 7. Counterexample summary submitted by GPT-6 Astra at max effort for the SlateDB WAL target ConsistentMachineData.

26

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

D

R EPRESENTATIVE S PECIFICATION F IXES

Section 4.1 summarizes the issues we found in source specifications during task construction. Table A15 lists representative issues. For each issue, we collect counterexamples and check each repair with model checking. We describe two of these cases in detail below. Table A15. Representative specification issues and their repairs. Specification

Issue

Repair

Status

OpenAddressing

With a single fingerprint, the divisor max(fps) min(fps) in the hash rescaling is zero. vars omits five of the 25 state variables, so stuttering steps can change them. 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. One transaction can start at two routers with different read timestamps, violating SnapshotIsolation (Section 4.1). Correct nodes accept a Byzantine leader’s proposal without a predecessor reference or a no-vote certificate, violating Agreement. A delayed writer’s fence, written after garbage collection, is skipped during replay, and ConsistentMachineData fails. Next has no action for splitting an inner node, so an insertion can deadlock.

Require a finite set of at least two fingerprints. Add them to vars.

Fixed upstream

Make replay and retry guards mutually exclusive.

Reported; no response

Check all routers before a transaction starts. Check the predecessor reference or no-vote certificate before admission. Validate the writer’s epoch after replay.

Fixed upstream

Not repaired; the five safety targets do not concern insertion progress. Acknowledge the replicated prefix, as the implementation does. Compare committed prefixes with later elections.

Acknowledged upstream

MongoDB Walgit WAL MongoDB Sailfish SlateDB WAL B-tree HashiCorp Raft

Replication acknowledgments report the follower’s whole log length instead of the replicated prefix.

etcd Raft

LeaderCompletenessInv compares leaders with the term that created an entry instead of the term that committed it.

Fixed upstream

Fixed upstream Reported; no response

Fixed upstream Fixed upstream

etcd Raft: a bug in the theorem. Raft’s leader completeness property says that an entry committed in some term appears in the log of every leader of a later term (Ongaro & Ousterhout, 2014). The original LeaderCompletenessInv (Example 8) instead compares a leader’s term with the term in which the entry was created. This theorem fails as Raft allows an entry to be committed late. The agent reported a counterexample with 47 transitions. We correct the theorem to talk about the committed term. We use commitHistory to record the term and committed log prefix whenever a server’s commit index advances, and electionHistory to record each leader’s term and log at election time. -LeaderCompletenessInv == \A i \in Server : LET committed == Committed(i) IN \A idx \in 1..Len(committed) : LET entry == log[i][idx] IN \A l \in CurrentLeaders : currentTerm[l] > entry.term => log[l][idx] = entry +LeaderCompletenessInv == + \A c \in commitHistory, e \in electionHistory : + c.term < e.term => IsPrefix(c.entries, e.entries) Example 8. Correction of the etcd Raft target LeaderCompletenessInv.

SlateDB WAL: a bug in the model. GPT-6 Astra disproved ConsistentMachineData on the original SlateDB WAL model with a 58-transition TLC counterexample (Example 7). After garbage collection deletes a DATA entry, a delayed writer writes a FENCE at the same position. Another writer replaying from an older snapshot skips the FENCE and enters READY without recovering the deleted data. We reported the trace upstream. Our revision adds a validation step

27

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

(Example 9): after replay, the writer reloads the latest log metadata and stops if a newer writer has taken over. The target properties are unchanged. On the revised model, Astra proves all four targets. ReplayWAL(w) == ... CASE id = wNextWalId[w] -> /\ wState' = [wState EXCEPT ![w] = READY] + /\ wState' = [wState EXCEPT ![w] = VALIDATE_AFTER_REPLAY] /\ wReplayId' = [wReplayId EXCEPT ![w] = 0] ... +ValidateEpochAfterReplay(w) == + /\ wState[w] = VALIDATE_AFTER_REPLAY + /\ CASE DoRefresh(w) -> + /\ RefreshManifest(w) + /\ UNCHANGED wState + [] ∼DoRefresh(w) /\ (wManifestLoad[w].valid = FALSE + \/ wEpoch[w] < wManifest[w].writerEpoch) -> + /\ wState' = [wState EXCEPT ![w] = FENCED] + /\ ManifestRefreshed(w) + [] ... \* (omitted: a newer local epoch leads to ILLEGAL_STATE) + [] ∼DoRefresh(w) /\ wManifestLoad[w].valid + /\ wEpoch[w] = wManifest[w].writerEpoch -> + /\ wState' = [wState EXCEPT ![w] = READY] + /\ ManifestRefreshed(w) + /\ UNCHANGED <<storeVars, gcVars, auxVars, wEpoch, + wNextWalId, wReplayId, wMachineData>> ... Next == ... \/ ReplayWAL(w) + \/ ValidateEpochAfterReplay(w) Example 9. Repair of the SlateDB WAL model (abridged diff, line breaks added).

28

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

E

AGENT P ROMPT AND S KILLS

We reproduce the proof construction prompt and the two agent skills supplied with the harness. The prompt is shown for etcd raft.tla. E.1

Proof Construction Prompt

The following prompt specifies the editable regions, available proof libraries, checker commands, and requirements for an accepted proof. Proof Construction Prompt # Task Prove every target theorem in etcd raft.tla. This is the only submitted file and represents one complete module task. Every supplied TLA+ context file in the workspace is read-only. You may create temporary wrappers, configs, traces, and other scratch files for local TLC or Apalache exploration. They are not submitted. Grading reconstructs a clean workspace from etcd raft.tla and the canonical read-only context, so the final task must not import or depend on scratch files. Only edit inside the `\* BEGIN AGENT HELPERS` ... `\* END AGENT HELPERS` region and each identified AGENT PROOF region (`\* BEGIN AGENT PROOF <proof-unit-id>` ... `\* END AGENT PROOF <proof-unit-id>`). Do not change the proof-unit IDs on the marker lines. You may choose the proof strategy and reuse any earlier sibling theorem once it is proved. Put fresh same-module operator definitions, module-level USE DEF or HIDE DEF directives, and fully proved named helper lemmas in AGENT HELPERS. Put each target theorem's proof only in its matching identified proof region. # Proving and iterating Audited official proof libraries are available at /opt/proof-libraries/tlapm and $COMMUNITY_LIB. Allowed modules are listed in $TLAPS_PROOF_LIBRARY_CATALOG. Inside AGENT HELPERS you may add LOCAL <alias> == INSTANCE <module> from that catalog, but you must not modify library files or use `WITH`. You may run: ˜˜˜sh /opt/tlapm/bin/tlapm -I /opt/proof-libraries/tlapm -I "$COMMUNITY_LIB" etcd raft.tla ˜˜˜ Keep refining the module until this authoritative check reports PASS: ˜˜˜sh check_proof_bin etcd raft.tla --mode proof-from-scratch ˜˜˜ Use this command without overriding `--timeout` or `--check-cpus`; it inherits the run's frozen verification policy. If a check reports a configuration error, follow its `RETRY-COMMAND` and obtain a proof-check result before submitting. Raw TLAPM and

29

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

Proof Construction Prompt `--sany-only` do not check the complete submission contract. The checker reports a raw result for every target and every helper theorem used by a target. A raw PASS counts only when all local theorem dependencies are also trusted, so a proof cannot rely on an omitted or circular sibling. Run the checker in the foreground and wait for that tool execution to finish. For a long-running tool call, use the tool's blocking wait facility rather than repeatedly launching checks or polling files. Each independent self-check has the same module budget as final grading; use `--check-session DIR` only when intentionally resuming one interrupted check of the unchanged candidate. A `NOT_STARTED` result means the module budget expired before that unit was checked, not that its proof failed. For a quick syntax check, run: ˜˜˜sh check_proof_bin etcd raft.tla --mode proof-from-scratch --sany-only ˜˜˜ If you must stop early, leave your best partial proofs in the module and run the authoritative check on that final file. Fix reported integrity violations, including edits to fixed whitespace, and rerun it after any correction. Independently trusted proof units still receive credit when the submission satisfies the integrity checks. # Constraints - Do not change the module header, imports, marker lines, theorem statements, theorem order, or any text outside the editable regions. - Do not modify or replace supplied dependency modules, and do not make the final task depend on scratch modules. - Do not add EXTENDS, nested modules, CONSTANT, VARIABLE, ASSUME, ASSUMPTION, or AXIOM declarations. INSTANCE is allowed only in the official-library form described above. - Every helper `LEMMA` or `THEOREM` must be named and fully proved. - Never use PROOF OMITTED or bare OMITTED, and never create a circular helper. - Bound the SMT/Z3 backend with a deterministic budget SMTT("rN"), capped at SMTT("r30"). Do not use the wall-clock forms SMT or SMTT(n). - New operator and lemma names must be fresh. Do not shadow names from the task or its context. - Do not browse or fetch external material. Work only from the files in this workspace and your knowledge of TLA+/TLAPS.

E.2

Agent Skills

Runs with the harness also receive the two agent skills described in Section 3.1, reproduced below. Skill: tlaps-proof-hints --name: tlaps-proof-hints description: Resolve TLAPS proof failures involving theorem instances from modules with

30

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

Skill: tlaps-proof-hints assumptions. Use when a citation such as BY I!Thm does not close a goal because prefixed and unprefixed imported operators are treated as different symbols. --# Use a theorem from an instantiated module ## Symptom A citation such as `BY I!Thm, NA` does not close the goal even though `I!Thm` appears to prove it and `NA` appears to supply the corresponding local assumption. ## Cause When a module with assumptions is instantiated as `I == INSTANCE M`, the instantiated assumptions become hypotheses of its theorem instances. If an assumption mentions an operator imported through `EXTENDS`, the instance re-exports that operator under the `I!` prefix. TLAPS treats the prefixed and unprefixed names as distinct internal symbols, so backends do not automatically relate `I!Pos(N)` to `Pos(N)`. ## Fix Prove a bridge theorem equating the prefixed operator with its local counterpart and cite it alongside the instantiated theorem: ```tla ---- MODULE Lib ---EXTENDS Integers Pos(n) == n > 0 ====

---- MODULE A ---EXTENDS Lib CONSTANT N ASSUME NA == Pos(N) THEOREM Thm == N > 0 BY NA DEF Pos ====

---- MODULE B ---EXTENDS Lib CONSTANT N ASSUME NA == Pos(N) I == INSTANCE A THEOREM Bridge == \A n : I!Pos(n) = Pos(n) BY DEF I!Pos, Pos

31

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

Skill: tlaps-proof-hints

THEOREM Test == N > 0 \* BY I!Thm, NA BY I!Thm, NA, Bridge ==== ```

\* FAILS \* WORKS

Source: [tlaplus/tlapm#279](https://github.com/tlaplus/tlapm/pull/279)

Skill: tla-inductive-invariant-validation --name: tla-inductive-invariant-validation description: Validate candidate inductive invariants for TLA+ safety proofs with Apalache or TLC. Use when designing or debugging an invariant, especially when TLAPS cannot discharge initiation, consecution, or safety-implication obligations. --# Validate a TLA+ inductive invariant Use a model checker to falsify a candidate invariant before investing in its TLAPS proof. Treat a successful finite check as evidence only: prove the invariant in TLAPS, and finish with the benchmark's authoritative `check_proof_bin` command. ## Run the three Apalache checks Shape the candidate as `IndInv == TypeOK /\ H`, where `TypeOK` contains one finite-domain membership clause for every variable and `H` contains the additional facts needed for induction. Given a target module `Target`, a typed wrapper `APTarget.tla`, and a safety predicate `Safety`, run: ```sh apalache-mc check --config=APTarget.cfg --init=Init --inv=IndInv --length=0 APTarget.tla apalache-mc check --config=APTarget.cfg --init=IndInv --inv=IndInv --length=1 APTarget.tla apalache-mc check --config=APTarget.cfg --init=IndInv --inv=Safety --length=0 APTarget.tla ``` Interpret these checks as: 1. `Init => IndInv`: legitimate initial states satisfy the candidate. 2. `IndInv /\ Next => IndInv'`: one step preserves the candidate. 3. `IndInv => Safety`: the candidate is strong enough to prove the goal. The checks starting from `--init=IndInv` require the candidate to assign every variable. A bare safety predicate can instead produce an assignment error such as `x' is used before it is assigned`. Write the missing `TypeOK` if the stripped target has none. Bound `Nat`-typed values to small finite sets, for example `num \in [P -> 0..4]`, and widen a bound before trusting a counterexample that may depend on it.

32

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

Skill: tla-inductive-invariant-validation When a check fails, read the counterexample. Apalache writes `violation1.tla` in a timestamped directory under `_apalache-out/<module>.tla/` unless redirected with `--out-dir` or `--run-dir`; the `Check the trace in: ...` log line gives the exact path. - A failure of the first check means the candidate excludes a legitimate initial state. - A failure of the second check gives a state satisfying `IndInv` and a successor violating it. The trailing `InvariantViolation` formula identifies the broken conjunct and usually exposes the fact missing from `H`. - A failure of the third check means the candidate does not imply the safety goal. Strengthen or correct the candidate from the trace, then rerun all three checks. ## Build a non-invasive Apalache wrapper Keep tool-specific annotations out of `Target.tla`. Re-declare its constants and variables with Apalache types in a separate wrapper, then instantiate the target: ```tla ---- MODULE APTarget ---EXTENDS Naturals CONSTANT \* @type: Int; N VARIABLE \* @type: Set(Int); active INSTANCE Target TypeOK == active \in SUBSET (0..N) H == TRUE IndInv == TypeOK /\ H ==== ``` Match every re-declared name exactly so implicit `INSTANCE` substitution binds it. Put each `\* @type:` annotation between the `CONSTANT` or `VARIABLE` keyword and the name it annotates, including every name originally declared in a multi-name block. A comment above the keyword is not accepted and leads to `Expected a type annotation for VARIABLE <name>`. Define `IndInv` in the wrapper. Fix finite constants in `APTarget.cfg`, for example: ```tla INIT Init NEXT Next CONSTANT N = 5

33

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

Skill: tla-inductive-invariant-validation ``` Alternatively, use `--cinit`. For an uninterpreted constant, define a finite value operator such as `JugVal` in the wrapper and substitute it with `Jug <- JugVal` in the configuration. If a polymorphic helper such as `Sum`, `Range`, or `ToSet` defeats type checking, shadow it in the wrapper with a monomorphic version. Only if the wrapper cannot be made to typecheck, annotate a private scratch copy: ```sh mkdir -p scratch cp Target.tla scratch/Candidate.tla ``` Never make the submitted solution extend or instantiate the wrapper or scratch module. Do not alter the target or any dependency as part of model-checking exploration. ## Fall back to TLC Use TLC when Apalache cannot type the target through a wrapper. Create a separate `MCTarget.tla` that extends `Target` and defines `TypeOK`, `H`, and `IndInv`, with `MCTarget.cfg` beside it. TLC is not on `PATH`; run: ```sh java -cp /opt/sany/lib/tla2tools.jar tlc2.TLC -deadlock -config MCTarget.cfg MCTarget.tla ``` Check the inductive step by making the candidate its own initial predicate: ```tla INIT IndInv NEXT Next INVARIANT IndInv ``` This checks `IndInv /\ Next => IndInv'` because `IndInv` is an ordinary invariant of the specification started in `IndInv`. Check `Init => IndInv` separately on the real specification with `SPECIFICATION Spec` and `INVARIANT IndInv`. Include `Safety` as a conjunct of `IndInv` to check that the candidate implies it. Use the same enumerable `TypeOK /\ H` shape as for Apalache. TLC first builds the states satisfying `TypeOK` and then filters them with `H`, so start with the smallest useful model. To reduce enumeration: - Move a conjunct of `H` immediately after the `TypeOK` clauses that bind the variables it mentions, allowing TLC to prune earlier. - Sample large domains with `RandomSubset(k, S)` from the `Randomization` module. Rewrite `v \subseteq W` as `v \in SUBSET W` and sample it with `RandomSetOfSubsets(k, p, W)`. Aim for a few dozen initial states. A TLC violation supplies the same useful two-state signal as Apalache. Once random sampling is involved, a run with no violation proves

34

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

Skill: tla-inductive-invariant-validation nothing; rerun it about a dozen times and abandon a run whose search depth grows beyond roughly a dozen steps. See Leslie Lamport's [Using TLC to Check Inductive Invariance](https://lamport.azurewebsites.net/tla/inductive-invariant.pdf) for the TLC technique. Never cite an Apalache or TLC verdict as justification for a TLAPS proof step.

35

Related documents

• Schwarz: Solver-Aware Agentic Program Verification#818849
• Schwarz: Solver-Aware Agentic Program Verification#808857
• Fixed point certificates for reachability and expected rewards in MDPs#1039242
• TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents#1325819
• Synthesizing Proofs Using Proof Sharding and Exploration#1076192