arXiv CSopen access

Specula: Scaling formal specifications for autonomous model checking of system code

Specula: Scaling formal specifications for autonomous model checking of system code Qian Cheng

Nanjing University Nanjing, China

Yiming Su

University of Illinois Urbana-Champaign, IL, USA

Ivan Beschastnikh

University of British Columbia Vancouver, Canada

Saad Mohammad Rafid Pial University of Illinois Urbana-Champaign, IL, USA

Emilie Ma

University of British Columbia Vancouver, Canada

Yu Huang

Nanjing University Nanjing, China

arXiv:2607.25333v1 [cs.SE] 28 Jul 2026

Finn Hackett

University of British Columbia Vancouver, Canada

Tianyin Xu

University of Illinois Urbana-Champaign, IL, USA

language takes months of effort, as it demands expertise of system design and implementation, maintenance of conformance between code and specification, let alone the mastery of TLA+ language and toolchains. As a result, our efforts were limited to specific system projects and are hard to scale. Recent advances of large language models (LLMs) and agentic AI, embodied by coding agents like Claude Code and Codex, show promise to scale formal specifications to any real-world systems and enable autonomous formal reasoning with minimal human intervention. Several recent studies reported that LLMs could generate formal specifications of different kinds [12, 37, 52, 56]. However, directly using LLMs or agents to generate formal specifications is fundamentally limited. First, LLMs make mistakes and could generate imprecise and even hallucinated specifications [11]. Adding human-in-the-loop to review auto-generated specifications is not only expensive but also unreliable. Moreover, as LLMs are known for reward hacking [18, 43], relying on LLMs to review and repair imprecise/incorrect specifications without well-defined boundaries is untenable. Furthermore, an inherent challenge, no matter whether for human or AI, is to decide the right level of abstractions to formally model complex systems [42]. We assert that these limitations are unlikely to be absorbed by the next-generation LLMs or agents, as they are not directly covered by the capabilities of LLMs.

Abstract Specula is a push-button agentic system that generates highquality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through selfevolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.

1

Ruize Tang

Microsoft Research Asia Beijing, China

Introduction

Formal specifications are key to automated correctness reasoning of large, complex software systems and are developed in practice to check and verify the designs of important systems [4, 8, 25, 32, 39]. Recently, formal specifications are further applied to system implementations, serving as abstractions of system code [42, 48]; these system specifications, empowered by model checking and theorem proving, help find deep bugs that manifest only under specific thread interleavings, message orderings, and/or partial failures. Despite their utilities, formal specifications are historically considered expensive to develop and maintain, especially for real-world systems with evolving codebases. In our prior work on specifying ZooKeeper and Asterinas [42, 48], writing high-quality specifications in the TLA+ specification

Contributions. We present Specula, a push-button agentic system that generates high-quality formal specifications for any large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs LLM-based agents to autonomously develop TLA+ specifications, including (1) invariants that describe correctness properties of the target system and (2) formal models that describe the system implementation with the right level of abstractions. Specula uses TLA+ as the default specification language for its current focus on distributed and concurrent systems which are critical infrastructures and desire automated formal reasoning. Specula equips its 1

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu

agents with skills and tools and enables them to use static analyzers, the TLC model checker [59], and trace validator (§4). Specula applies to system code written in any programming language as it abstracts the code in the TLA+ model. Specula is fully autonomous in developing formal specifications and eliminates the barrier of applying formal methods to real-world system code. Specula automatically checks the conformance between the formal TLA+ model of the system and the system code, eliminating classic model-code gaps [6]. The conformance checking is achieved by automated trace validation [13, 22, 48], where the agents autonomously instrument system code, collect traces, and validate generated TLA+ model using code-level traces. If the TLA+ model fails trace validation, Specula autonomously repairs the model or the code instrumentation until model-code conformance. Specula anticipates mistakes and errors, as well as rewardhacking behaviors, introduced by LLMs in generating specifications, including both system models and invariants. Specula crafts self-evolving loops where the agents iteratively improve specification quality. In ambiguous situations, e.g., an invariant violation can be caused by incorrect modeling, bugs in the code, wrongly inferred invariants, or their combinations, the evolving loops enable agents to deepen their understanding of system code and its behaviors and pinpoint true root causes. To prevent reward hacking (e.g., overfitting a system model to match code-level traces), Specula defines clear boundaries by pairing trace validation and model checking—the former ensures that the model admits code-level behaviors and the latter rejects invalid states. Specula models system implementations with the levels of abstractions guided by the invariants it inferred from the system artifacts (e.g., code, comments, documents, and userreported issues). As a principle, it abstracts out behaviors irrelevant to the correctness properties while describing important details that must be carefully modeled. It thus can generate multiple system models with different abstractions for different kinds of invariants, balancing efficiency (avoiding state-space explosion) and utility (bug finding). With the specification in place, Specula checks system code by systematically exploring the formal model and checks on violations of invariants (which indicate bugs in the code). For each violation, Specula further replays it at the code level based on the model-level traces and encapsulates it in a system test to help developers reproduce the bugs reliably.

no false positive as all the bugs are reproduced at the code level. We reported 89 bugs; so far, 68 have been confirmed and 24 have been fixed. Specula has been used by several companies. The Specula project is maintained at: https://github.com/specula-org/Specula.

2

Background

2.1

Formal specification and model checking

Specula targets concurrent and distributed systems and thus chooses TLA+ as the specification language. TLA+ is a language for writing formal models as abstractions of programs; it is not specific to any implementation languages like C/C++, Java, Rust, etc. TLA+ has been widely used for checking system designs and distributed protocols in practice [25, 39]; recently, it is also used for checking code-level behaviors by extracting models from code [11, 42, 48]. A TLA+ specification comprises two parts: a model that describes behaviors of the system and invariants that define its correctness properties. The model specifies system behaviors as a collection of state variables, an initial predicate that defines their initial values, and a next-state relation that determines state transitions. The next-state relation is expressed as multiple actions, each describing an atomic state update of the variables. An invariant is a property that must hold in every reachable state of the model. Figure 1a shows a source-code snippet in C++ of the Raft implementation in ScyllaDB, which is a part of the handler code a node runs upon receiving log entries from the leader. The handler appends the entries to its local log 1 , and then advances its commit index, which is capped by std::min 2 to stay within the entries it actually holds. Figure 1b shows the TLA+ model of the code snippet as an action (generated by Specula). It is enabled when an append-entries message is pending, and describes steps 1 and 2 that update the state variable commitIndex following the control flow of the code. The invariant CommitIndexSafety defines the correctness property the model must maintain: log entries that any node has committed agree with a non-stale leader’s log. TLA+ specifications can be verified using explicit-state model checking via TLC [59] and symbolic model checking via Apalache [28]. Specula uses TLC which systematically explores all reachable states of the model to ensure that the invariants hold over the entire state space. When an invariant is violated, TLC returns a counterexample, a sequence of actions from an initial state to the violating state. The number of reachable states grows combinatorially with the number of state variables and the size of the model. Hence, the cost of model checking, in terms of both time and memory, is a key consideration that drives specification design [42]. For TLA+ models that describe system implementations, the model must conform to the code. Conformance is commonly checked via trace validation [4, 13, 22, 48]. Trace validation checks whether execution traces collected from the

Key results. We maintain Specula as an open-source project. Specula currently supports agents such as Claude Code, Codex, and Copilot CLI with different LLMs. We have used Specula (with a default configuration of Claude Code with Opus-4.8) to check 48 open-source system projects, including both distributed systems (e.g., MongoDB, Etcd, and ScyllaDB) and concurrent systems (e.g., GCC libgomp and LLVM libomp). Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula reports 2

Specula: Scaling formal specifications for autonomous model checking of system code void fsm::append_entries(...) { 1

2

System Code

index_t last_new_idx = request.prev_log_idx; if (!request.entries.empty()) { last_new_idx = _log.maybe_append(std::move(request.entries)); } advance_commit_idx( std::min(request.leader_commit_idx, last_new_idx)); }

Invariants (safety, liveness)

an agent with new information, e.g., a counterexample, a model-code gap, a reproduction failure, etc.

/\ LET lastNewIdx == m.mprevLogIdx + Len(m.mentries)

Limitations of AI agents. Our experience tells that directly using AI, even with the strongest LLMs, is fundamentally limited. First, the codebase of large, complex systems often exceeds what an agent can hold in context. As a result, AIgenerated TLA+ models often misrepresent the implementation: they hallucinate execution paths, oversimplify concurrency, and fall back on TLA+ models in training sets [11]. We found that AI often generates models that omit important behaviors while admitting states the system never reaches. Second, AI agents have no reliable basis to determine the right level of abstraction without expert guidance. Historically, human experts make empirical decisions based on intuition and experience [42]. Too high-level models are less useful (e.g., for finding deep bugs in code), while too low-level models include unnecessary details that lead to state space explosion. It is even harder for agents to discover invariants. Real-world code rarely states them, and for wellknown protocols agents often default to textbook invariants even where the implementation deliberately deviates. Lastly, reward hacking is still a severe problem of frontier AI. When the agent is rewarded for a given goal (e.g., trace validation), it can overfit the specification by weakening invariants or manipulating TLA+ models only for the purpose of matching expected traces. Such a behavior often results in imprecise models, leading to false results. Unfortunately, reward hacking is often subtle and hard to catch.

\* Max: commitIdx only moves forward newCommitIdx == Max(commitIndex[i], Min(m.mleaderCommitIdx, lastNewIdx)) IN /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIdx]

(b) The TLA+ action that models the code snippet in (1a) CommitIndexSafety == \A i \in Server : state[i] = Leader => \A j \in Server : \A idx \in 1..commitIndex[j] : \* snapshot-index guards elided currentTerm[i] >= LogTerm(j, idx) => LogTerm(i, idx) = LogTerm(j, idx)

(c) A safety invariant of the above code snippet—a non-stale leader’s log matches every entry each node has committed.

Figure 1. An example of TLA+ specification, including (1b) model and (1c) invariant of (1a) the source code snippet in C++ (from the Raft implementation of ScyllaDB). running system code correspond to paths in the model’s state space. The traces are obtained by instrumenting the system code. A trace the model rejects pinpoints where the model and the code diverge. Figure 2 shows the classic process of formal specification and model checking. 2.2

TLC Model Checking

Figure 2. The classic process of formal specification and model checking; specifications are written by human experts.

HandleAppendEntriesRequest(i, j, m) == /\ m.mtype = AppendEntriesRequest /\ ... 2

TLA+ System Spec

Conformance checking (trace validation)

(a) Code snippet in C++

1

Write

AI for Formal Specification

3

AI agents have proven effective at software engineering. A coding agent can autonomously read large codebases, explain how code paths behave, and carry out tasks such as code generation and bug fixing [9, 53, 58]. These capabilities extend to formal specification: recent benchmarking finds that coding agents produce TLA+ models that pass syntax and runtime checks, capture essential system behavior, and reproduce known bugs in five real-world systems [12]. An increasing paradigm of agentic AI is to organize them as evolving loops, where the agent accumulates knowledge and improves its capabilities over iterations based on feedback of previous iterations [40, 45]. It is reported that evolving loops improve coding agents across tasks such as debugging and program repair [5, 10]. Specula organizes coding agents as self-evolving loops (§3.5): each iteration presents

Specula Design

Specula is a push-button agentic system that generates formal specifications for any given system and uses the specifications for model checking and bug finding. The specification of a system generated by Specula includes (1) a formal model that effectively describes the implementation of the target system and (2) invariants that describe the correctness properties the target system must hold. Specula then uses the generated specifications to check the system implementation—it systematically explores the formal model and checks on violations of invariants (which indicate bugs in the code). For each violation, Specula further replays it at the code level based on the model-level traces. Specula autonomously generates formal specifications from the artifacts of the target system (e.g., its repositories) 3

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu

using LLM-based coding agents such as Claude Code and Codex. Specula aims to generate formal specifications that: • precisely and comprehensively describe safety and liveness invariants the system must hold, including invariants at the implementation level that are not described in the protocol (if any); • effectively model the system by describing important codelevel behaviors that are critical to find deep bugs while making the model tractable for model checking to avoid state-space explosion; • conform to the system code so that model checking results are sound and can be reproduced at the code level. Specula iteratively improves formal specifications till they meet aforementioned criteria. Our key insight is that, with the capabilities of frontier LLMs and agents (§2.2), generating formal specifications is no longer laborious and timeconsuming as before (a coding agent can generate quality TLA+ specifications in seconds [12]); however, generating precise, comprehensive, and effective formal specifications with no model-code gap is still fundamentally challenging and is beyond raw capabilities of frontier LLMs/agents. Specula is designed to provide agents with an effective process to guide the generation of formal specifications at the right abstraction, and rigorous harness to evolve the specifications to achieve model-code conformance and bug reproduction. Specula targets concurrent and distributed systems which have complex, non-deterministic behaviors and desire automated formal reasoning. Specula uses TLA+ as the formal specification language and uses TLC [59] as the model checker, which are widely used for checking and verifying concurrent and distributed systems [12, 13, 42, 47, 48]. In principle, Specula could support any other specification languages but we have only experimented with TLA+ . 3.1

\* Any committed entry is on a majority's durable storage CommittedInDurableStorage == \A s \in Server : commitIndex[s] <= durable_storage[s]

(a) Protocol-level invariant generated by Specula for Etcd-Raft \* Any committed entry is on a majority's log (in memory) CommittedInLog == \A s \in Server : commitIndex[s] <= Len(log[s])

(b) Code-level invariant generated by Specula for MongoDB

Figure 3. Invariants summarized by Specula from artifacts “committed entries are durable and will eventually be executed by all of the available state machines [41].” Etcd-Raft’s implementation follows this invariant. Specula also infers code-level invariants from system code, test cases, issues, and revision histories. Specula equips the agent with a skill and few-shot examples that capture common patterns of code-level property, such as atomicity of operations, bounded capacity of data structures, and monotonicity of commit index; it analyzes test cases to understand scenarios and the expected behavior; it also reads scenarios described by user-reported issues and pull requests which often describe faults and the expected behavior. Note that the agents are instructed to focus on summarizing invariants on system-level behaviors; they do not produce low-level invariants on API or variables (e.g., non-pointers). Figure 3b shows a code-level invariant Specula generated for MongoDB whose replication follows the Raft protocol. In this case, Specula finds that MongoDB does not strictly follow the Raft protocol and thus the CommittedInDurableStorage invariant in Figure 3a does not apply. To optimize write latency, MongoDB can be configured to report an entry to be committed once a majority holds it in memory, before flushing it to stable storage. The design deliberately gives up the durability guarantee, with a weaker one: a server never reports an entry committed before that entry is written in its own log. Specula derives this invariant from the revision history in which MongoDB began deciding commitment from the in-memory log rather than from stable storage [1]. Each invariant is associated with a fault model, which would guide the fault injection during model checking (§3.4). Specula enforces the AI agents to provide concrete evidence where it derived the invariants from (e.g., code, issues, commits, and comments). The lineage enforces the agents to generate grounded invariants and is also used in the selfevolving loop that involves improving invariants (§3.5).

Understanding correctness properties

Specula starts from understanding the correct properties of the target system. The correctness properties guide specification generation (§3.2)—the TLA+ model of the system should preserve necessary details that can affect the properties and abstract out the others. The correctness properties are embodied in invariants under fault models. Specula instructs AI agents to summarize two kinds of invariants from the system artifacts: protocol-level invariants1 and code-level invariants, as shown in Figure 3. Specula then encodes these invariants in TLA+ . The protocol-level invariants are typically sourced from protocol descriptions, system documentation, and source code. For example, for a Raft implementation, protocol-level invariants often include Election Safety, Log Matching, Leader Completeness, etc. [41]. Figure 3a shows a protocol-level invariant Specula generated for Etcd-Raft, which states that

3.2

Generating effective system models

With correctness properties, Specula generates TLA+ models of the system. An effective model is tractable for model checking to explore its state space within a practical budget, and

1We take a broad definition of protocol and assume each system is imple-

mented based on an explicit or implicit protocol.

4

Specula: Scaling formal specifications for autonomous model checking of system code

has high utility for finding code bugs. Historically, human experts make decisions on what to omit and to model. Recent work proposes to customize TLA+ models by specifying system modules in different abstraction levels [42]. Specula uses agentic AI to fundamentally reduce the cost of generating TLA+ models (see §2) and ensuring their code conformance (§3.3). With the low cost of generating highquality models, Specula pushes the principle of model customization to a new level—it generates customized models for important scenarios; these scenario-based models help model checking to focus on the system’s most significant and potentially vulnerable behaviors, increasing the likelihood of detecting bugs that may only manifest under specific conditions. Concretely, Specula maintains a reference model of the target system (§3.2.1) and projects it to customized models based on the scenarios it generates (§3.2.3).

Scenario. Joint consensus quorum tracking on voter demotion: Evidence: history: Three fixes reworked joint-config voter tracking (8f64a6d2d2, f31f73b1e8 #10618, b3cb4f3966) code: * broadcast_read_quorum (fsm.cc:1052) sends a read quorum to followers whose cached vote flag is set * set_configuration (tracker.cc:101) sets that flag from the current config * committed<read_id> (tracker.cc:178) commits a read on acks from both current and previous voter sets Modeling proposal: variables: * config[s]: (current, previous) configs * voters[s][c]: voters in config c * canVote[s]: cached send-path flag actions: EnterJoint, LeaveJoint, ReadBarrier, ... invariant: ReadBarrierProgress -- an issued read barrier eventually commits

Figure 4. A simplified modeling plan produced by Specula’s analysis for ScyllaDB’s Raft library.

3.2.1 Reference model. Specula instructs AI agents to generate a reference TLA+ model by reading and understanding the system code together with auxiliary materials in the artifact such as documents and test cases. Specula lets AI agents autonomously determine the abstraction levels of different parts of system code based on the correctness properties (§3.1)—the reference model must describe all the behaviors relevant to each invariant and omit others. For example, data structures of hash implementations are typically abstracted out; however, for Papaya (a concurrent hash map) Specula explicitly models the per-slot meta byte and entry pointer to check the invariant on no lost entry. In contrast, the hash function itself stays out of the model, as no invariant depends on it. Invariants guide the abstraction level, but they do not determine the semantics of the selected behavior. Once Specula models certain parts of the implementation, it derives the state representation and transition relation from the code. Model variables correspond to implementation fields and data structures, and each action follows the guards, branches, and state updates at specific program points. Figure 1 shows how Specula models the append-entries handler of ScyllaDB-Raft (written in C++) using a TLA+ action, guided by an invariant on the leader’s commitIndex. The resulting TLA+ action mirrors the original control flow. The aforementioned generation alone does not ensure the code conformance of the reference model. Specula ensures conformance by conformance checking and repair (§3.3).

that describes the scenario—making the scenario auditable and minimizing hallucination. Each scenario description also lists the related variables, actions, and invariants (which are used to generate scenario-based models). Figure 4 shows a scenario of joint-consensus reconfiguration during voter demotion in ScyllaDB, where a node is voter in the previous configuration but non-voter in the current one. Specula creates this scenario because it observes that (1) the related code has been changed by multiple fixes and (2) the fixes are inconsistent in different code snippets. In fact, this scenario enabled Specula to discover a new bug that stalls a read barrier during voter demotion, which violates the ReadBarrierProgress invariant. 3.2.3 Scenario-based models. For each scenario, Specula generates a TLA+ model as a projection of the reference model—it only describes behaviors relevant to the target scenario, which is a subset of the behaviors the reference model admits. Each scenario-based model simplifies certain actions and behaviors in the reference model by rewriting the corresponding ones, while directly invoking the others; the reference model is immutable. The projection is in principle sound: any invariant violation it finds is also a violation in the reference model. The projection takes three steps (as exemplified in Figure 5):

3.2.2 Generating scenarios. Specula automatically generates scenarios from the system artifact, instead of relying on developers as in prior work [32, 42, 48]. In our experience, state-of-the-art agents have strong capabilities of summarizing a comprehensive set of scenarios that are described in documents and comments, discussed in reported issues and revision history, and encoded in test cases. Specula enforces the AI agent to provide evidence when generating a scenario— specific commits, issues, comments, or other information

1. Selecting actions. Specula enables only actions needed to exercise the scenario and bounds the occurrence of those actions. In Figure 5a, the scenario disables crashes (CrashLimit = 0) and keeps lease reads (ReadRequestLimit = 2), focusing the search on the stale-leader read path. Setting an action’s bound to 0 disables that action. 2. Coarsening actions. Specula can replace a multi-step process in the reference model with a coarse action, if the behavior is required by the scenario but not the targeted 5

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu CrashLimit = 0 ReadRequestLimit = 2 ...

\* disabled: limit is 0

HandleAppendEntriesRequest(i, m) == /\ logOk \* Overfitting repair: overwrite suffix unconditionally /\ log' = [log EXCEPT ![i] = SubSeq(log[i], 1, prevLogIndex) \o entries] /\ commitIndex' = [commitIndex EXCEPT ![i] = Min(leaderCommit, Len(log'[i]))]

MCCrash(s) == /\ crashCount < CrashLimit \* always false /\ Crash(s) \* never fires /\ crashCount' = crashCount + 1

\* Correct repair: truncate only where entries conflict /\ log' = [log EXCEPT ![i] = IF EntriesMatch(i, m) THEN log[i] ELSE SubSeq(log[i], 1, prevLogIndex) \o entries]

(a) Action selection. Wrapping an action with a counter that bounds its occurrences. Setting the counter to 0 disables the action. MCNext == \/ \E s \in Server : MCLeaderElection(s)

(a) The overfitted repair (red) and the correct repair (green) of the follower’s accept path in Kudu-Raft.

\* removed: BecomeCandidate, RequestVote, ... \/ ...

StateMachineSafety == \A i, j \in Server : \A n \in 1..Min(commitIndex[i], commitIndex[j]) : log[i][n] = log[j][n]

MCLeaderElection(s) == /\ \A t \in Server : state[t] # Leader /\ \E Q \in Quorum : /\ s \in Q /\ \A t \in Q : LogUpToDate(s, t) /\ state' = [state EXCEPT ![s] = Leader] /\ ...

(b) Protocol-level invariant (State Machine Safety)

Figure 6. An overfitted repair and the protocol-level invariant that exposes it. To replay a trace, the agent overwrites the follower’s log suffix unconditionally (red); this passes trace validation but lets a delayed append-entries message truncate a committed entry, which violates State Machine Safety. The correct repair (green) truncates only on conflicts.

(b) Action coarsening. Replacing multiple actions with one atomic action. Intermediate states are abstracted out. MCNext == \/ \E s \in Server : MCReadyAndSend(s) \* removed: Ready, FlushPendingResponses (separate) \/ ...

from each action/variable in model to the corresponding program location in the code during modeling (§3.2). Specula also repairs the models that fail conformance checking.

MCReadyAndSend(s) == Ready(s) \cdot FlushPendingResponses(s)

(c) Serialization. Serializing two actions into one atomic transition via TLA+ action composition (\cdot).

3.3.1 Trace validation. Specula implements automatic trace validation in three steps. First, Specula uses AI agents to emit an instrumentation plan based on the input model. For each TLA+ action, the plan lists the action’s origin in the code, a triggering point related to a designated operation, and the state variables to capture. Second, Specula uses the agent to instrument the system implementation at the origin location with calls to a tracing library that records, for each action invocation, the action name and the captured state. Third, Specula instructs the AI agent to generate a TLA+ replay harness in which every model-level action is wrapped to match the incoming event, execute the code-level action, and check that the post-state agrees with the recorded snapshot. TLC then checks the harness against collected traces, advancing one event at a time until the trace is exhausted. Any failures of trace validation mean that the model does not conform to the code and must be repaired.

Figure 5. Three projection operations applied to Etcd-Raft’s LeaseRead stale-read scenario. behavior. Figure 5b shows MCLeaderElection replacing the full voting protocol with one atomic action that picks a node whose log is up-to-date for a majority. The reference model’s election semantics are preserved (only valid leaders are chosen), but the votes, timeouts, and re-candidacies are skipped. 3. Shaping action sequences. Specula can constrain an action to a particular phase of the execution, forcing them to be atomic (if intermediate states are irrelevant) or otherwise encode the ordering assumptions of the target scenario. Figure 5c shows one such pattern. 3.3

3.3.2 Repairing models. The key challenge of repairing models that fail trace validation comes from the fact that AI agents tend to overfit the model to match traces by weakening guards, adding permissive transitions, or even hardcoding trace-specific state updates. For example, a voting action that allows a node to vote for any candidate can make election traces replay successfully, but it admits behaviors

Ensuring model-code conformance

Specula ensures model-code conformance of both reference and scenario-based models by trace validation [13, 42, 48]. Historically, trace validation is costly due to code instrumentation (for producing code-level traces), which often requires manual efforts [42]. Specula automates instrumentation as the model is generated from the code; it records the mapping 6

Specula: Scaling formal specifications for autonomous model checking of system code

against voting rules in the implementation. In essence, trace validation checks that code-level actions can occur in the model, but it does not explore whether the model also admits illegal actions. (This was less a problem in the past as human experts would not repair models by overfitting.) Specula therefore uses bidirectional validation to converge the model and the code toward conformance. Our insight is that model checking can be used to restrict the model correctness and prevent overfitted repairs. Specula model-checks the repaired model against protocollevel invariants (§3.1), to capture incorrect overfitted repairs. Figure 6 shows an example from Kudu-Raft, where modelchecking the repaired model against an invariant on State Machine Safety exposes an overfitted repair. Note that Specula does not assume AI-generated invariants and repaired models are always correct; Section 3.5 describes how Specula handles those issues.

that triggers the bug: an external thread completes a detached task only after every other thread has parked in the barrier’s wait loop, at which point the wake-up fails to mark the barrier’s task as pending and no thread can finish the barrier. Specula inserts a sleep in the external thread with precise timing, turning a race into a deterministic deadlock. (This bug was introduced in 2021 and only found by Specula.) In the case Specula failed to reproduce the buggy behavior after the four phases of attempts, Specula instructs the agents to understand the reason based on the code-level traces produced during the reproduction. If the agent thinks that the model trace cannot be reproduced at the code level (e.g., certain branch conditions are missed in the model), Specula restarts model repair (§3.3.2). If the agent thinks the reason is the difficulty of deterministic replay (e.g., it requires external control), Specula preserves the analysis and evidence for the user. Empirically, Specula reliably reproduced 98% of the violations it judged to be real bugs.

3.4

3.4.2 Comprehending buggy behaviors. Specula observes the system-level impact of buggy behaviors to understand their consequences. Specula first checks whether the reproduced execution leads to an observable consequence such as data loss, a crash, a deadlock, or a wrong output. If none occurs, Specula does not discard the violation; it instructs the agents to read issue discussions, design documents, tests, and comments, and interprets the violation in that context. In our experience, Specula’s prediction on the consequence is reasonable, interpretable, and evident.

Finding and reproducing buggy code behavior

After achieving model-code conformance, Specula modelchecks each scenario-based model against the protocol- and code-level invariants under the fault model. An invariant violation may indicate a bug in the code. Specula first runs TLC in breadth-first mode [59], which exhaustively covers every behavior up to a predefined depth. Many bugs lie deeper than breadth-first search within the time budget. Specula therefore complements it with TLC’s simulation mode [59], which samples long random traces. 3.4.1 Reproducing buggy code behavior. Specula attempts to reproduce buggy code behavior using the model trace and encapsulate the reproduction in a test. Since the model trace describes the exact sequence of events that triggers the invariant violation, reproduction is not a search over any schedules but a controlled task of forcing one known schedule onto a code execution. Specula instructs the agents to control (1) faults and (2) the order of events (controlled by adding sleep between events). Specifically, the AI agent writes a test, observes the order of events, and compares it against the target sequence in the trace. The procedure is tedious but mechanical. Specula enforces a structured search by instructing agents to reproduce the behavior in four phases: (1) interacting with the system via its client APIs, (2) adding sleep between the API calls to control concurrency externally, (3) crafting preconditions in terms of system state (e.g., a value left by a crash fault), and (4) adding sleep in system code to control internal concurrency. The agent stops at the phase that can reproduce the target behavior. Specula forbids shortcuts that would craft the violation such as preloading illegal state, directly calling private functions, or changing system code logic. For example, Specula can deterministically reproduce a deadlock in libgomp (GNU Offloading and Multi Processing Runtime Library). Model checking finds the thread schedule

3.5

Self-evolving loops

We have not systematically discussed how to address mistakes or errors introduced by AI agents—every component in Sections 3.1–3.4 is powered by AI agents and thus is subject to hallucinations [27, 54] and knowledge gaps (e.g., due to limited context windows) [26, 34]. Specula does not assume inherent correctness of any outputs of AI agents. Instead, it carefully devises self-evolving loops that enable AI agents to correct erroneous invariants, formal models, and code instrumentation. As a key design principle, for each loop iteration, Specula enforces AI agents to collect new information and reason about its outputs with more evidence, thus gradually enhancing the agents’ understanding of the target system. In this way, the agents are improving and unlikely to make similar mistakes. 3.5.1 Loop structure. Figure 7 shows the self-evolving loops across the components in Specula. We mainly discuss two interdependent loops that involve model-code conformance (§3.3) and buggy behavior reproduction (§3.4). Conformance loops. To achieve model-code conformance, the AI agents continuously evolve the reference and scenariobased models through a loop of trace validation and model checking. The former ensures that code-level behaviors are 7

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu

Invariant incorrect

Generating TLA+ models (§3.2)

Reproducing buggy behavior (§3.4)

3.5.2 Correctness. The evolving loops are safe—they should not incorrectly reduce Specula’s bug-finding capabilities. First, the loop between trace validation and model checking only gradually tightens model-code conformance without relaxing invariants. Second, for the conformance loop that revises protocol-level invariants, the updated invariants are expected to become more precise, with detailed understanding of why the original protocol-level invariants are incorrect. Third, for the reproduction loop that revises invariants, the updated invariants are expected to reflect code-level correctness properties more closely. Note that revising invariants requires AI agents to provide strong evidence that the original invariants were incorrect or unnecessary; it is not used as a way to work around violations. With the assumption that agents improve over the iterations, Specula offers convergence—the invariants eventually converge and the agents eventually evolve the TLA+ model that conforms to system code. In practice, we run Specula under a budget in time or cost. In our evaluation, an end-to-end run takes 1.43 to 9.86 hours across the target systems.

Invariant incorrect

Generating invariants (§3.1)

Conformance checking (§3.3) Repair

Model checking

Trace validation

Invariants

Code instrumentation

Incorrect state transition

Bug report

Figure 7. Specula’s self-evolving loops

permitted by the model, while the latter prevents agents from repairing models by overfitting code-level traces (§3.3). With right invariants, the agents would evolve till the generated TLA+ models permit all code-level traces and satisfy protocollevel invariants (or it finds a code bug). As a tricky situation, when a repaired model fails a protocollevel invariant, there can be a combination of three cases: (1) the model is still incorrect, (2) there is a code bug that fails the invariant, and (3) the invariant is incorrect. Specula instructs the agent to reason about the three cases and decide the corresponding action: (1) continuing to repair the model, (2) reproducing the bug (see §3.4), and/or (3) correcting the invariant, and then redoing model generation and conformance checking (§3.1–§3.3). In our experience, agents typically judge (3) correctly, when enforced by Specula to provide concrete evidence from code, comments, and other artifacts as justifications. In fact, if agents make mistakes on invariants, the process would not converge but continue to iterate. On the other hand, agents often have difficulty differentiating (1) and (2), as both surface a model state that violates invariants—the code alone does not directly show whether the state can be reached at the runtime. If the agent mistakenly treats (2) as (1), it will tighten the model to exclude the state, which will later be rejected by trace validation. If the agent mistakenly treats (1) as (2), the mistake will be surfaced during bug reproduction.

4

Implementation

Specula is built on coding agents such as Claude Code, Codex, and Copilot CLI. It includes about 5.5K lines of Markdown Agent Skills and 24.8K lines of code across Python, UNIX shell, and Java, for supporting tools and orchestration. Each component (see Figure 7) is implemented as a multiagent workflow: a primary coding agent equipped with specific skills and tools, who may spawn more agents for scoped subtasks. The components are orchestrated as producers and consumers—a component can consume outputs (in file format) produced by other components. These files can be used as checkpoints for retrying a component or forking multiple instances of a component (e.g., for processing multiple specification variants). Each component runs coding agents inside a shared workspace that contains the target system artifact and component specific workspaces. Tools. Besides standard CLI tools like UNIX shells, Specula equips its agents with TLA+ tools: (1) the SANY parser [30], (2) the TLC model checker [59], and a static analyzer we wrote for checking if each action correctly specifies an atomic transition over all declared variables (an important feature missed by SANY and TLC [2]). Together, these tools let agents catch and correct common mistakes such as missing UNCHANGED clauses, duplicate assignments, inconsistent action structures, and malformed configuration files. For code instrumentation, Specula offers the agent a trace library we wrote. The trace library exposes per-language emit functions for agents to insert at each instrumentation point to record a trace event. The agent uses the trace library with the system’s build and test tools to insert trace events in the code. For distributed systems, Specula uses a mutex-based recording mechanism, following prior work [13, 42, 47]; for

Reproduction loops. Specula reproduces buggy code behavior event by event (§3.4). If the agents cannot reproduce events, it restarts the conformance loops with the diverging states as the feedback (Figure 7): it is possible that conformance checking missed rare cases due to its incompleteness. If reproduction succeeds but no observable consequence occurs (§3.4.2), it indicates three cases: (1) the invariant is overly strong, (2) the consequence is masked by the system’s built-in mitigation/recovery modules, and (3) the agent fails to reproduce the bug. Specula instructs the agents to reason about the three cases and choose to (1) improve the invariant, which may trigger redo of model generation and conformance checking (§3.1–§3.3), and (2) provide evidence and report to users (masked violations still indicate bugs), and (3) report to users and let them judge. 8

Specula: Scaling formal specifications for autonomous model checking of system code

5

80

Bugs

15 BFS (187) Simulation (13)

10 5 0

60 40 20

0

10

20

30

40

Counterexample length

50

0

Figure 8. Counterexample lengths of the 200 bugs found via model checking. BFS returns the shortest counterexample; Simulation does not. The CDF curve covers all 200 bugs. the number of bugs found by Specula per system. Note that only the highlighted results reflect the latest Specula (our v1.0 release); the other results are from early versions of Specula; we expect the latest Specula would find more bugs (we are limited by our budget to rerun everything). As Specula is instructed to target core logic of concurrent, distributed systems, which desires formal methods and model checking, the bugs found by Specula are deep with severe consequences, including:

Evaluation

Our evaluation aims to answer the following questions: 1. Is Specula effective in finding important, deep bugs? 2. How do Specula’s capabilities of specification and bugfinding compare to standard agentic approaches? 3. What is the cost of using Specula to check a system? 4. How effective are Specula’s self-evolving loops (§3.5) in correcting mistakes? 5. How sensitive is Specula’s effectiveness to the capabilities of the coding agent it uses?

• Deadlocks and system hangs, e.g., GCC’s libgomp can run into deadlocks due to a missing flag on a barrier wakeup path (§5.1.2); • Data loss or corruption, e.g., MongoDB’s sharding module marks the wrong migration task as ready, leading to incorrect data deletion; • Crashes and component failures, e.g., ra, the Raft library of RabbitMQ’s quorum queues, crashes a follower process when a new leader overwrites an uncommitted membership change on a regular log entry; • Loss of availability, e.g., in HashiCorp’s Raft library, which underlies Consul and Vault, a leader whose disk has stalled keeps sending heartbeats that suppress elections, so the cluster can neither commit nor fail over.

We apply Specula to 48 system projects, including 36 distributed systems and 12 concurrency systems. The evaluated projects include widely used open-source projects such as MongoDB and GCC libgomp, as well as artifacts from research papers like Autobahn [19]. A full list of evaluated systems can be found in Table 1. These systems span seven different languages (including C, C#, C++, Erlang, Go, Java, and Rust) with various sizes (2K to 95K LoC). For all the experiments, we ran Specula with Claude Code v2.1.97 (Claude Opus-4.8, 1M context window, with max reasoning) on an Azure VM with a 96-core AMD EPYC 9V74 CPU and 384 GB of RAM. Each run executes in an isolated git workspace that symlinks to the target system project. 5.1

100

median 9

Cumulative %

concurrent systems, Specula uses a timebox-based recording mechanism [24] that captures per-thread operation intervals and lets validation search for an ordering consistent with the intervals, minimizing the impacts of instrumentation. For trace validation, Specula offers the agent a trace inspector and a debugger. The inspector provides APIs for agents to query events, variables, and time windows and return matching states with optional in-situ evaluation of specification expressions on that state. A trace may contain thousands of lines; loading the full trace into the agent’s context is inefficient. Hence, we wrote a debugger [38] that supports breakpoints, hit counts, expression evaluation, and variable inspection, letting the agent pause validation at any point and inspect any specification expression or runtime state. This is useful, because raw trace validation reports only the depth at which TLC stops, not the failure state; also, the true divergence may originate in an auxiliary variable that drifted many actions before the reported point. The debugger lets the agent walk back to the specific transition where the divergence began and trace how it propagated through subsequent actions till the violation.

Among the 249 bugs Specula found, 200 (80.3%) surfaced through model checking; the rest was found during code comprehension and modeling only. Of the 200 bugs surfaced by model checking, 187 were found by breadth-first search (BFS), which returns the shortest counterexample. Figure 8 plots the distribution of these counterexample lengths with a median of 9 steps and a p90 of 18 steps. The other 13 were found by random simulation whose traces are not shortest. BFS sufficed for 187 (93.5%) of the 200 violations, showing that Specula’s scenario-based decomposition keeps each model’s state space tractable enough for model checking to reach the bug within a bounded time budget. Most (99.10%) invariants Specula generates across the 48 systems are safety properties. Only 0.90% are liveness properties. Specula mostly checks liveness through TLC’s deadlock

Bugs found

We treat bug finding as one utility of Specula. We have applied Specula to 48 system projects in the course of its development (many were by requests). In total, Specula found 249 bugs in the 48 systems: 207 were new bugs and 42 were known bugs (but not fixed). We reported 89 bugs; so far, 68 have been confirmed and 24 have been fixed. Table 1 shows 9

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu

Table 1. The numbers of bugs found by Specula in each evaluated system. “New” refers to new bugs and the numbers in “()” refer to bugs that were confirmed by the developers. The shaded rows are results from the latest Specula version. System

Type

Lang.

Aptos Quorum Store AptosBFT arc-swap async-raft Autobahn Babylon Besu QBFT braft CometBFT crossbeam-deque crossbeam-epoch crossbeam-skiplist dotNext dpdk-ring Dragonboat eliben-raft Epaxos etcd/raft GCC libgomp go-algorand goraft HashiCorp Raft HotShot kanal left-right libspdm LLVM libomp MongoDB N2Paxos nebula (Raft) NuRaft papaya rabbitmq/ra raft-java RedisRaft RethinkDB (Raft) scc ScyllaDB (Raft) sofa-jraft Solana SONiC spdm-rs Substrate Sui SwiftPaxos tikv/raft-rs tokio-broadcast willemt/raft

BFT BFT Concurrency Raft BFT BFT BFT Raft BFT Concurrency Concurrency Concurrency Raft Concurrency Raft Raft Paxos Raft OpenMP BFT Raft Raft BFT Concurrency Concurrency SPDM OpenMP Database Paxos Database Raft Concurrency Raft Raft Raft Database Concurrency Database Raft BFT Network OS SPDM BFT BFT Paxos Raft Concurrency Raft

Rust Rust Rust Rust Rust Go Java C++ Go Rust Rust Rust C# C Go Go Go Go C Go Go Go Rust Rust Rust C C++ C++ Go C++ C++ Rust Erlang Java C C++ Rust C++ Java Rust C/C++/Rust Rust Rust Rust Go Rust Rust C

Total

New

Total

2 (0) 1 (0) 2 (1) 8 (0) 16 (15) 4 (0) 2 (1) 4 (0) 10 (0) 2 (1) 0 (0) 1 (0) 4 (2) 1 (0) 1 (0) 4 (3) 3 (0) 1 (0) 3 (2) 2 (0) 5 (0) 2 (2) 5 (0) 3 (0) 2 (0) 25 (16) 1 (0) 15 (0) 3 (0) 2 (0) 3 (0) 4 (1) 7 (7) 2 (0) 2 (0) 1 (1) 0 (0) 1 (1) 10 (3) 0 (0) 19 (1) 10 (8) 0 (0) 2 (0) 2 (2) 3 (1) 2 (0) 5 (0)

2 1 7 8 16 6 3 5 15 2 2 2 4 1 1 4 3 2 3 2 5 3 5 3 3 26 1 15 3 2 3 4 7 5 2 2 1 1 10 8 25 10 1 2 2 4 2 5

207 (68)

249

Table 2. Distribution of sources of evidence Specula cited when generating invariants across evaluated projects. One invariant can have multiple sources. Source of evidence Implementation code and comments Issue trackers, pull requests, and advisories Prior fixes, commit history, and tests Documentation and reference literature

Invariants 87.35% 74.34% 42.88% 20.04%

but never makes progress. Table 2 shows the percentages of sources Specula derives invariants from. Among these invariants, 21.1% are at the protocol level and 78.9% are at the code level (§3.1). 5.1.1 False positives. For the 14 systems checked with the latest Specula (shaded in Table 1), Specula reported 136 bugs. For 134 of them, Specula reproduced the violations at the code level and encoded them in a test (§3.4). For the remaining two bugs, Specula also reproduced both of them, but did not observe severe consequences; so, Specula considered them as bugs that were masked by the system. 5.1.2 Case studies. We present two case studies, where we use Specula to check GCC libgomp and SONiC which represent real-world concurrent and distributed systems. GCC libgomp. The GNU Offloading and Multi-Processing library (aka libgomp) is the runtime library of GCC for sharedmemory parallel programming. Its low-level concurrency is hard to reason about and the developers asked us to help model-check it using Specula. We ran Specula on an unmerged patch that adds a faster barrier, directing the agent to focus on it. Specula surfaced two bugs (Figure 9): one introduced by the patch and one latent in an existing barrier. The run took about six hours of compute and 1.5 hours of human review to confirm the bugs. The first bug (Figure 9a) resides in the fast barrier implementation. libgomp encodes the barrier’s round counter and its status flags in an integer; one of those flags is for pending cancellation (BAR_CANCELLED). When the barrier advances to the next round, a helper recomputes this integer from the counter bits alone, wiping every flag, then restores only the flag that increment sets. However, it never restores BAR_CANCELLED, so a cancellation in flight at that moment reaches only some of the threads. Those threads stop, while the rest see the barrier complete normally and keep running. The result is a split-brain and the patch developer confirmed and fixed this bug. The second (Figure 9b) is a deadlock that had been latent in the codebase for at least five years. For the two paths that wake a barrier thread, one omits the call that marks tasks pending, so a woken thread can return to sleep with work still queued. The same developer confirmed it.

detection, which works in both BFS and random simulation. For a small number of models whose state space can be exhausted, Specula checks the temporal formulas directly, reporting a liveness violation when the model’s fairness assumptions still admit an execution that keeps taking steps 10

Specula: Scaling formal specifications for autonomous model checking of system code

Table 3. Examples of bugs Specula found in SONiC modules

gomp_increment_gen(unsigned gen, int incr) { gens = gen & BAR_BOTH_GENS_MASK; // flags wiped ... case BAR_HOLDING_SECONDARIES: return gens | BAR_HOLDING_SECONDARIES | (gen & BAR_CANCELLED); // keep cancel }

Modules

Bug

dash-ha

Teardown of a group misses noti- The components keep actfications to components using it ing on deleted state

(Rust)

✗ Safety invariant: A BAR_CANCELLED flag, which was set, must be carried by the barrier’s advance to the next round.

(a) Cancellation flag dropped when the barrier finishes.

fdb (C++)

Removing a lookup entry before hardware invalidation

iccpd (C)

An incorrect sync drives the pro- The coordination of two tocol into an error state switches fails

linkmgrd

A startup case is missing from the failover logic

(C++)

omp_fulfill_event(omp_event_handle_t event) { if (new_tasks > 0) { // path 1 gomp_team_barrier_set_task_pending(...); do_wake = ...; } if (!do_wake && waiting_for_tasks(...)) { gomp_team_barrier_set_task_pending(...); do_wake = 1; } }

Consequence

Inconsistency between software and hardware

The link is left stuck with no recovery

warmreboot Reporting recovery complete be- Forwards traffic using fore a dependency is restored state that is not yet rebuilt

(C++)

mlacp_sync_send_all_info_handler(csm) { ... // first send all sync data to the peer if (MLACP(csm).current_state < EXCHANGE) MLACP(csm).current_state++; // stay in FSM }

✗ Liveness invariant: Any wake-carrying tasks must set the pending flag; otherwise the woken thread sleeps and causes deadlocks.

(b) A wake path omits set_task_pending.

✗ Safety invariant: once the two peers finish the handshake (state EXCHANGE), a later sync request must not change the protocol state.

Figure 9. Two bugs Specula found in libgomp and the codelevel invariants they violate.

(a) In iccpd, a re-sync after the handshake turns the state machine into an unrecoverable ERROR state. // setup path notifies every scope actor: notify_scope(HaSetState { up: true }); // teardown must send the matching down: notify_scope(HaSetState { up: false });

Both bugs surface only under specific thread interleavings. The deadlock needs a parked thread to be woken because work is still outstanding, rather than through the common path taken when a new task is created. The cancellation bug needs a cancellation in flight at the moment the leader thread advances the barrier and pauses the other threads. Such interleavings are hard for ordinary tests to produce, so the bugs went undiscovered; model checking enumerates all interleavings and captures the triggering path.

✗ Safety invariant: tearing down an HA set must notify every actor its setup did, so none keeps a stale up state.

(b) In dash-ha, teardown misses sending notifications to actors that were previously notified with the HA setup.

Figure 10. Two bugs Specula found in SONiC which violate protocol-level (iccpd) and code-level (dash-ha) invariants.

SONiC. SONiC is a network operating system used primarily for switches in datacenter networks. It has multiple modules, from programming the switch’s forwarding hardware to running peering protocols to recovering state after reboots. We ran Specula on five modules, written in C++, C, and Rust, with no module-specific tuning. Specula produced TLA+ specifications for each and the model checking surfaced at least one bug in each module (see Table 3). Figure 10 shows two bugs. In Figure 10a, iccpd keeps two switches in sync: a handshake first advances a state machine into the operational EXCHANGE state. The handler that sends a peer its sync data ends by advancing this state machine, which is correct during the handshake but also runs on a subsequent re-sync. Taken in EXCHANGE, that extra advance overshoots into an ERROR state with no recovery, and the switches stop coordinating until the connection resets. In Figure 10b, dash-ha notifies every dependent actor when initiating an HA set, but incorrectly notifies no actor when tearing the HA down. As a consequence, the actors rely on an HA set that no longer exists. Neither bug is reachable

by the project’s tests (the former needs a precise message ordering, the latter needs a test that exercises the teardown path which does not exist). Model checking finds both and Specula reproduces them at the code level. 5.2

Comparison with other agentic approaches

We compare Specula against two agentic approaches as our baseline (all three approaches use the same prompts): • Agent-Raw. Claude Code without additional Skills or MCPs. Agent-Raw represents the raw LLM’s ability without using domain-specific tools. • Agent-TLA+ . Claude Code equipped with the TLA+ Skills and MCPs [29]. Agent-TLA+ represents official tools for syntax checking and model checking. Unlike Specula, Agent-TLA+ is not designed with techniques for modelcode conformance or self-evolving loops to correct model or invariant errors. 11

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu

Table 4. Specification quality measured by SysMoBench [12]. Agent

Syntax Runtime Conform. Inv. Overall

Specula (Opus-4.8) Agent-Raw Agent-TLA+

100% 100% 100%

100% 79% 82%

100% 70% 75%

100% 84% 82%

100% 81% 82%

Specula (Sonnet-4.6) 100% Specula (Haiku-4.5) 95%

100% 56%

90% 51%

90% 17%

93% 47%

Agent-Raw

Specula (Haiku-4.5)

0

2

Specula

3

(Opus-4.8)

62

10

Agent-TLA+

Specula (Sonnet-4.6)

Figure 11. Comparative analysis of bug finding of different approaches. The default LLM is Claude Opus-4.8.

For this analysis, we select Autobahn, CometBFT, libspdm, MongoDB, and sofa-jraft—written in Rust, Go, C, C++, and Java respectively (see Table 1). We compare the quality of generated TLA+ model, the bugs found, and the false positives of the three approaches.

Table 5. Cost (in USD) to check a system project on average and the corresponding running time (in minutes) for Specula, compared with Agent-Raw and Agent-TLA+ . Agent-Raw

Quality of the generated TLA+ model. We use

5.2.1 SysMoBench [12] to evaluate the quality of the reference model generated by Specula and the other two agentic approaches (see §3.2.1). SysMoBench requires human-verified invariants as inputs and thus cannot evaluate invariants; we manually wrote the invariants for the five evaluated systems. SysMoBench introduces four metrics of model quality: (1) syntax correctness, (2) runtime correctness (if the TLA+ model could run without exceptions), (3) model-code conformance, and (4) invariants (if the generated model satisfies invariants), with an aggregated overall score. Table 4 shows the results. Specula achieves perfect scores on SysMoBench, while Agent-Raw and Agent-TLA+ do not. All three approaches write perfect TLA+ syntax. However, Agent-Raw and Agent-TLA+ cannot ensure runtime correctness or model-code conformance (Agent-TLA+ achieves higher scores by using tools). Specifically, we find that the official TLA+ tools bring no real improvement overall: what is lacking is not TLA+ knowledge but the runtime feedback that helps the agents to repair and revise the models.

System

Time

Autobahn CometBFT libspdm MongoDB sofa-jraft

27 40 14 15 11

Agent-TLA+

Cost Time $5.99 $6.27 $3.81 $3.82 $2.19

Specula

Cost Time

69 $16.46 13 $2.58 16 $5.08 15 $4.26 24 $4.91

Cost

110 $28.96 402 $167.83 151 $40.75 157 $47.54 199 $81.06

checking reports a violation which is not a bug. In another case, an Agent-Raw-generated model admits a behavior the code rules out, such as a message arriving after a client has unsubscribed. libspdm’s behaviors hinge on small, scattered details which are more fine-grained than in the other projects. Modeling without grounding against the code, Agent-Raw and Agent-TLA+ drop these details and report violations that those details would rule out in the implementation. 5.3

Cost

For the 48 systems, Specula takes 1.43–9.86 hours to check each system end-to-end, with a median of 3.69 hours; these end-to-end checks cost $19–$168 US dollars of token consumption, with a median of $57 US dollars. We consider the monetary cost to be reasonable, considering the month of efforts human experts need to pay for writing specifications by hand [8, 16, 25], let alone model checking, trace validation, and bug reproduction. Reducing the token cost is an active future work. For example, many subtasks do not need the strongest LLM and could be routed to cheaper ones. Table 5 shows the token cost and running time for the five systems studied in §5.2, compared with Agent-Raw and Agent-TLA+ . Across the 19 modules of the five systems, Specula costs $50.73 and takes 2.8 hours on average. This is about 4.8–37× more expensive than Agent-Raw and 1.8–65× than Agent-TLA+ . Most of the cost falls in TLA+ model generation and code instrumentation. We find that the token cost is more strongly correlated to the complexity of the target system than its size. The cost of checking modules is not evenly distributed—a few complex modules are significantly more expensive to check.

5.2.2 Bugs found. As shown in Figure 11, Specula finds 62 bugs, while Agent-Raw finds 2 and Agent-TLA+ finds 3. The reason Specula found more bugs is threefold. First, Specula builds more effective TLA+ models that describe important code-level behaviors related to the invariants, while the other approaches often abstract important behaviors out. Second, Specula generates models for relevant scenarios, letting model checking explore the state space more effectively. Third, Specula models more invariants, checking correctness properties the others do not. The results show the importance of effective, targeted formal specifications. 5.2.3 False positives. Specula reports no false positives; Agent-Raw reports five and Agent-TLA+ reports two. The false positives reported by Agent-Raw and Agent-TLA+ all come from incorrect specifications when checking libspdm. In one case, Agent-Raw generates an invariant stronger than the implementation guarantees, assuming a certificate is verified where the protocol makes no such promise, so model 12

Specula: Scaling formal specifications for autonomous model checking of system code

The two longest runs are CometBFT and libspdm’s cert auth, which drive far larger searches than any other module. For example, in CometBFT’s PBTS module, the coding agent took 670 agent steps for checking and repairing the TLA+ model, more than 4× the other modules, and TLC generated 1.9 billion states while visiting 393 million distinct ones. 5.4

Bugs found. With Sonnet-4.6, Specula finds 10 of the 62 bugs it finds with Opus-4.8 (Figure 11). With Haiku-4.5, it finds none. With Sonnet-4.6, Specula found bugs in Autobahn, CometBFT, and libspdm (none in MongoDB or sofajraft). With Sonnet-4.6, Specula analyzes the artifacts less deeply and thus it builds a less complete model; it also validates the model less thoroughly, so the model records fewer of the code-level behaviors. With Haiku-4.5, the workload outstrips the LLM: Specula frequently stops, declaring the task done before finishing it. Cost. With Sonnet-4.6, Specula takes nearly the same time as with Opus-4.8 (188 vs. 166 minutes per module on average), and spends 61% of the budget, yet finds 16 of the bugs: about $59 per bug found, against about $16 with Opus-4.8. With 1 Haiku-4.5, Specula costs 17 as much per module as with Opus-4.8, but finds nothing. False positives. A weaker LLM visibly deviates from Specula’s instructions. With Sonnet-4.6, 39 false bugs reached the reproduction phase. Among 33 of them, Specula followed the instructions: it attempted the reproduction as instructed, watched it fail, and eventually realized that they were not true bugs. On the other six, it hacked the reproduction to make it succeed by injecting illegal states directly to the running system. Reward hacking of such is explicitly disallowed by the instructions. With the same instructions, Specula with Opus-4.8 exhibits no such violation.

Effectiveness of self-evolving loops

Agents routinely make mistakes. For all the 48 evaluated systems, Specula has to repair the TLA+ model it generates (§3.3.2). For 36 systems, invariants were revised; for 33 systems, code instrumentation was corrected. Therefore, the self-evolving loops are essential. The conformance loop caught and repaired three kinds of agent mistakes on invariants (17.3%), code instrumentation (22.2%), and model (60.5%) (§3.5). Of the violations that entered reproduction, 47.5% reproduced as real bugs, and 48.8% were discharged with evidence drawn from the system itself and fed back to repair the model or its invariants. The agents reported the remaining cases to users; only 1.0% are considered bugs it cannot reproduce. All our recorded Specula runs converged. Code instrumentation errors were repaired within three rounds, and 91.3% of invariant and model errors were fixed in one iteration; none in more than four. The one case that took four revisions came from SONiC’s link manager, where Specula generated an incorrect invariant that a link’s two gateways are never both on standby. Differentiating a bug from a legitimate transient is hard: in each round, model checking surfaced a different valid case, such as a failover handoff or a degraded mode where neither gateway can take over, and after four counterexamples the agent arrived at a correct invariant. 5.5

6

Discussion

Durable design. The development of Specula has coincided with rapid advancement of LLM capabilities. Earlier LLMs and agents often failed to produce high-quality TLA+ specifications without substantial repair efforts, while recent LLMs can carry much more of the modeling work on their own. This shift shaped our view of Specula’s design—the system should not be limited by specific LLM/agent generations, but should improve as the LLMs/agents improve. The durable core of Specula is to treat system artifacts as the ground truth. The agents decide the invariants and behaviors to model from the system artifact and check them against code bi-directionally: trace validation confirms the model admits code-level executions, and model checking exposes states the model incorrectly allows. Model-level violations return to code, where reproduction decides whether they are true bugs or not. This structure remains necessary as LLMs improve, because hallucination, overgeneralization, and reward hacking are unlikely to disappear. Evolving with LLMs/agents. With the durable design, the implementation of Specula carries optimizations we made to leverage the capabilities of the current coding agents. Specula’s skills and tools are equipped to compensate for specific weaknesses of LLMs or coding agents today, and we expect to evolve them when LLMs/agents improve. Take bug reproduction (§3.4) as an example. Reproducing a bug

Sensitivity to coding agents

We measure Specula’s sensitivity to the underlying coding agents by applying Specula to the same five system projects in §5.2, with two different LLMs, Claude Sonnet-4.6 and Haiku-4.5 (which have weaker capabilities than Opus-4.8). Quality of TLA+ models. We use the same methodology to evaluate the quality of generated TLA+ models as in §5.2.1. Table 4 shows the results. Specula with Sonnet-4.6 achieved syntax and runtime correctness and its overall quality is higher than those generated by Agent-Raw and Agent-TLA+ with Opus-4.8. However, with Sonnet-4.6, Specula was not able to achieve complete conformance and invariant correctness (90% each): its model replays fewer of the implementation’s traces, and some of the invariants fail on it even though the invariants it wrote hold. With Haiku-4.5, Specula fails earlier. Specula asks more of the LLM than plain specification generation, and with Haiku-4.5 it already struggles to produce a model that runs: MongoDB’s specification fails syntax correctness, and on average TLC can execute only about half of the actions in its models. 13

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu

at the code level is a durable design, but how we let the agent achieve the reproduction is not. Asked to reproduce a violation, a current coding agent often hacks out a success: it injects a faulty state directly or calls internal functions out of context. Specula therefore restricts reproduction to behaviors an external client can trigger, and forbids reward hacking. With restrictions in place, frontier agents produce almost no false positives and follow the instructions, while a weak LLM may not (§5.5). As LLMs/agents become even more capable, the way Specula carries out bug reproduction can further improve.

more tractable but requiring human experts to write the model, choose the action granularity, and check conformance with code. Recent work [20, 42, 48] develops multiple system models at different levels of abstractions to help model checking focus on target modules (e.g., the changed ones). Specula follows this practice using an agentic approach. Unlike prior work that relies on human experts to decide the levels of abstractions, Specula autonomously makes the tradeoff between utility and efficiency based on target invariants. Model-code conformance. There are two common ways of conformance checking: replaying models at the code level [42, 47] and validating code-level traces against the model [13, 16, 25, 44, 49]. Early refinement-style validation requires strict state and action mappings between code and its model [16, 44]. Recent work [13, 24, 25, 48] relaxes this requirement by using TLA+ ’s nondeterminism to infer missing states and compose actions to align granularity, e.g., OmniLink [24] validates code-level traces without requiring each API call to have a single observed linearization point. Specula uses trace validation to align generated models with code across different action granularities and abstraction levels. Compared with traditional approaches, it automates instrumentation and trace checking. Moreover, Specula couples trace validation with model checking to catch overly permissive model repair that trace validation alone would accept.

Resolving issues iteratively. Several components in Specula produce artifacts whose correctness is hard to guarantee at the time they are generated, e.g., code instrumentation, TLA+ models, and invariants. Instead of forcing each artifact to be correct in local context, Specula accepts imperfect ones and resolves issues iteratively through self-evolving loops. For example, Specula generates invariants, without establishing that they must hold for the implementation, at the time it extracts invariants from the system repository (§3.1). This is a deliberate design because demanding a correct invariant upfront is overly difficult at the moment the agents know little about the system implementation. When an invariant does not hold, resolving it in the loop forces an investigation that deepens the agent’s understanding of the system (§3.3). Formal guarantee. Specula carries a few common limitations of AI-driven autonomous techniques—it is hard to provide formal guarantees of the behaviors and results of LLMbased agents. For example, Specula reads and comprehends the system artifacts (e.g., its software repository) to decide what to model; there is no formal guarantee that it models everything perfectly as the modeling is autonomously driven by the agents. Similarly, the invariants Specula extracts may not capture every property a system should hold. A model can therefore remain inconsistent with the implementation in ways we did not catch, and a bug that depends on such a gap can remain undetected.

7

AI-based specification generation. AI-based specification generation has mostly followed the deductive verification approach for sequential programs, where specifications are program annotations such as preconditions, postconditions, and loop invariants [37, 52, 56]. Recent work also translates natural-language descriptions into formal specifications [7, 15]. Model checking instead requires specifications that define a behavioral model and properties to check. Recent work also uses agents to construct and repair formal models, e.g., Event-B Agent synthesizes and repairs Event-B models from requirements using formal-tool feedback [51]. Specula extracts both invariants and a model of the system from the target’s own artifacts. It uses coding agents’ semantic understanding of the artifacts and generates scenarios that reduce the state space to explore in model checking.

Related Work

Model checking. Model checking aims to exhaustively explore the state space of abstractions of actual programs [14] and is shown to be effective for reasoning about real-world systems [39, 42, 47, 48]. For concurrent and distributed systems, TLA+ is commonly used to check system design and implementation [23, 25, 39, 59]. Applying model checking to real-world systems must carefully balance the cost of writing and maintaining formal specifications, state space, and model-code conformance. Implementation-level model checking [21, 31, 36, 57] avoids modeling effort by exploring state space directly at the code level; however, with enormous details of code behaviors, it is hard to bound the state space in a general way. Specification-based approaches [25, 42, 47, 48] lift exploration to a formal model, making state exploration

Formal-methods agents. Recent agents use formal methods concepts or tools to guide bug finding. FM-Agent uses a top-down approach to derive natural-language function specifications from callers and applies AI-based Hoare-style reasoning over code blocks to flag violations [17]. BMC-Agent performs per-function bounded model checking by translating inferred pre/postconditions into CBMC/Kani harnesses, then validates and refines counterexamples [46]. Specula differs by moving the reasoning target from function-level source code to system-level behaviors. It targets distributed and concurrent system bugs expressed as protocol- and codelevel invariant violations, using self-evolving loops to repair model, invariant, and instrumentation errors. 14

Specula: Scaling formal specifications for autonomous model checking of system code

Recent agents target auto-generation of formal proofs in Lean, Coq/Rocq, Dafny, and Verus [3, 33, 35, 50, 55]. These agents use verifier feedback to refine a formal artifact until the verifier accepts it. These works can provide stronger guarantees than bug finding, but are scoped to the behaviors captured by the formalization and proof obligations. Specula makes a different tradeoff: it prioritizes autonomous, lowcost specification and discovery of complex distributed and concurrency bugs, where system-wide deductive verification remains challenging and limited by practical constraints.

8

the IEEE/ACM 47th International Conference on Software Engineering (ICSE’25) (Apr. 2025). [6] Brooker, M. Fifteen Years of Formal Methods at AWS. In TLA+ Conference (Apr. 2024). https://youtu.be/HxP4wi4DhA0. [7] 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’25) (July 2025). [8] Cauli, C., Lang, T., Chen, S., Mouelhi, S., Jin, X., Bandopadhyay, S., Chen, X., Feng, Y., Song, H., Tang, L., Sheng, Z., and Srinath, A. S. Lessons Learned from Incorporating Formal Methods in Huawei Cloud Reliability. In Proceedings of the 21st European Conference on Computer Systems (EuroSys’26) (Apr. 2026). [9] Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H. P., Kaplan, J., et al. Evaluating Large Language Models Trained on Code. https://arxiv.org/abs/2107.03374, 2021. [10] Chen, X., Lin, M., Schärli, N., and Zhou, D. Teaching Large Language Models to Self-Debug. In Proceedings of the 12th International Conference on Learning Representations (ICLR’24) (May 2024). [11] Cheng, Q., Tang, R., Ma, E., Hackett, F., He, P., Su, Y., Beschastnikh, I., Huang, Y., Ma, X., and Xu, T. Can LLMs model real-world systems in TLA+? https://www.sigops.org/2026/can-llms-model-real-worldsystems-in-tla, May 2026. [12] 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’26) (Apr. 2026). [13] Cirstea, H., Kuppe, M. A., Loillier, B., and Merz, S. Validating Traces of Distributed Programs against TLA+ Specifications. In Proceedings of the 2024 International Conference on Software Engineering and Formal Methods (SEFM’24) (Nov. 2024). [14] Clarke, E. M., and Emerson, E. A. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Logic of Programs, Workshop (Oct. 1981). [15] Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., and Trippel, C. nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. In Computer Aided Verification (CAV’23) (July 2023). [16] Davis, A. J. J., Hirschhorn, M., and Schvimer, J. eXtreme Modelling in Practice. Proceedings of the VLDB Endowment (VLDB’20) (May 2020). [17] Ding, H., Wang, Z., and Chen, H. FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning. https://arxiv. org/abs/2604.11556, 2026. [18] Gao, L., Schulman, J., and Hilton, J. Scaling Laws for Reward Model Overoptimization. In Proceedings of the 40th International Conference on Machine Learning (ICML’23) (July 2023). [19] Giridharan, N., Suri-Payer, F., Abraham, I., Alvisi, L., and Crooks, N. Autobahn: Seamless high speed bft. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (SOSP’24) (Nov. 2024). [20] Gu, X., Cao, W., Zhu, Y., Song, X., Huang, Y., and Ma, X. Compositional Model Checking of Consensus Protocols via InteractionPreserving Abstraction. In Proceedings of the 41st International Symposium on Reliable Distributed Systems (SRDS’22) (Sept. 2022). [21] Guo, H., Wu, M., Zhou, L., Hu, G., Yang, J., and Zhang, L. Practical Software Model Checking via Dynamic Interface Reduction. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP’11) (Oct. 2011). [22] Hackett, F., and Beschastnikh, I. Tracelinking implementations with their verified designs. Proc. ACM Program. Lang. (Oct. 2025).

Remarks

Our goal of developing the Specula project is to expand the outreach of formal methods to improve the correctness and reliability of system software, with the astonishing capabilities of today’s AI agents. A key principle is to exploit the generative capabilities of AI to lower the cost of formal specifications, while addressing the new challenges introduced by AI for specification generation. Specula shows that a fully autonomous formal-methods system can be built with careful design and implementation, and it is feasible to achieve a reliable specification technique atop imperfect (and often unreliable) AI agents. Specula is under active development (hence we decide not to have a conclusion section). We encourage everyone to try it out, for fun and profit!

Acknowledgements The Specula project started from a hackathon effort to compete the GenAI-accelerated TLA+ Challenge in 2025. We thank the TLA+ Foundation for organizing the challenge and recognizing our work. We thank Markus Kuppe for continuously supporting the project and for the invaluable discussions. We thank Neil Giridharan for helping us understand our results of Autobahn. We thank everyone who gave us feedback and/or encouragement along the development of Specula, including Zhizhen (Cathy) Cai, Zhiting Zhu, Matthew Malcomson, Dmitry Kulagin, Claudia Cauli, Timo Lang, Igor Konnov, Chris Newcombe, and Darko Marinov.

References [1] MongoDB SERVER-85701: Use lastWritten opTime for commit point calculation when writeConcernMajorityJournalDefault is false. https: //jira.mongodb.org/browse/SERVER-85701. [2] Static syntax check of UNCHANGED keyword. https://github.com/ tlaplus/tlaplus/issues/677, Oct. 2021. [3] Banerjee, D., Bouissou, O., and Zetzsche, S. DafnyPro: LLMAssisted Automated Verification for Dafny Programs. https://arxiv. org/abs/2601.05385, 2026. [4] Bornholt, J., Joshi, R., Astrauskas, V., Cully, B., Kragl, B., Markle, S., Sauri, K., Schleit, D., Slatton, G., Tasiran, S., Van Geffen, J., and Warfield, A. Using lightweight formal methods to validate a key-value storage node in amazon s3. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles (SOSP’21) (Oct. 2021). [5] Bouzenia, I., Devanbu, P. T., and Pradel, M. RepairAgent: An Autonomous, LLM-Based Agent for Program Repair. In Proceedings of 15

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, and Tianyin Xu [23] 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 (ICSE-SEIP’23) (May 2023). [24] Hackett, F., Wrench, E., Macko, P., Davis, A. J. J., Wei, Y., and Beschastnikh, I. Trace Validation of Unmodified Concurrent Systems with OmniLink. https://arxiv.org/abs/2601.11836, 2026. [25] 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’25) (Apr. 2025). [26] Hsieh, C.-P., Sun, S., Kriman, S., Acharya, S., Rekesh, D., Jia, F., Zhang, Y., and Ginsburg, B. RULER: What’s the Real Context Size of Your Long-Context Language Models? In Proceedings of the 1st Conference on Language Modeling (COLM’24) (Oct. 2024). [27] Ji, Z., Lee, N., Frieske, R., Yu, T., Su, D., Xu, Y., Ishii, E., Bang, Y., Madotto, A., and Fung, P. Survey of Hallucination in Natural Language Generation. ACM Computing Surveys (2023). [28] Konnov, I., Kukovec, J., and Tran, T.-H. TLA+ Model Checking Made Symbolic. Proceedings of the ACM on Programming Languages 3, OOPSLA (Oct. 2019), 1–30. [29] Kuppe, M. A., and Kulagin, D. tlaplus/agentskills, Mar. 2026. [30] Kuppe, M. A., Lamport, L., and Ricketts, D. The TLA+ Toolbox. In Proceedings of the 5th Workshop on Formal Integrated Development Environment (F-IDE’19) (Oct. 2019). [31] Leesatapornwongsa, T., Hao, M., Joshi, P., Lukman, J. F., and Gunawi, H. S. SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI’14) (Oct. 2014). [32] Li, A., Desai, A., and Padhye, R. Feedback-guided Adaptive Testing of Distributed Systems Designs. In Proceedings of the 23rd USENIX Symposium on Networked Systems Design and Implementation (NSDI’26) (May 2026). [33] Liu, J., Zhou, Z., Zhu, Z., Dos Santos, M., He, W., Liu, J., Wang, R., Xie, Y., Zhao, J., Wang, Q., Zhi, L., Li, J., and Li, W. Numina-LeanAgent: An Open and General Agentic Reasoning System for Formal Mathematics. https://arxiv.org/abs/2601.14027, 2026. [34] Liu, N. F., Lin, K., Hewitt, J., Paranjape, A., Bevilacqa, M., Petroni, F., and Liang, P. Lost in the Middle: How Language Models Use Long Contexts. Transactions of the Association for Computational Linguistics (TACL) (2024). [35] Liu, Y., Wan, X., Wang, Y., Wang, M., Huang, L., and Wei, T. KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code. https://arxiv.org/abs/2605.03822, 2026. [36] Lukman, J. F., Ke, H., Stuardo, C. A., Suminto, R. O., Kurniawan, D. H., Simon, D., Priambada, S., Tian, C., Ye, F., Leesatapornwongsa, T., Gupta, A., Lu, S., and Gunawi, H. S. FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. In Proceedings of the 14th European Conference on Computer Systems (EuroSys’19) (Mar. 2019). [37] Ma, L., Liu, S., Li, Y., Xie, X., and Bu, L. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE’25) (Apr. 2025). [38] Microsoft. Debug adapter protocol, 2026. [39] Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., and Deardeuff, M. How Amazon Web Services Uses Formal Methods. Commun. ACM (Mar. 2015). [40] Novikov, A., Vũ, N., Eisenberger, M., Dupont, E., Huang, P.S., Wagner, A. Z., Shirobokov, S., Kozlovskii, B., Ruiz, F. J. R., Mehrabian, A., Kumar, M. P., See, A., Chaudhuri, S., Holland, G., Davies, A., Nowozin, S., Kohli, P., and Balog, M. AlphaEvolve: A Coding Agent for Scientific and Algorithmic Discovery.

https://arxiv.org/abs/2506.13131, June 2025. [41] Ongaro, D., and Ousterhout, J. In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Annual Technical Conference (USENIX ATC’14) (Oct. 2014). [42] 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’25) (Mar. 2025). [43] Pan, A., Bhatia, K., and Steinhardt, J. The Effects of Reward Misspecification: Mapping and Mitigating Misaligned Models. In Proceedings of the 10th International Conference on Learning Representations (ICLR’22) (Apr. 2022). [44] Pressler, R. Verifying Software Traces Against a Formal Specification with TLA+ and TLC. https://pron.github.io/files/Trace.pdf, 2018. [45] Sharma, A. OpenEvolve: An open-source implementation of AlphaEvolve. https://github.com/codelion/openevolve, 2025. [46] Sun, Y., Liu, J., Kroening, D., and Xue, J. Agentic Model Checking. https://arxiv.org/abs/2605.21434, 2026. [47] Tang, R., Sun, X., Huang, Y., Wei, Y., Ouyang, L., and Ma, X. SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration. In Proceedings of the 19th European Conference on Computer Systems (EuroSys’24) (Apr. 2024). [48] 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 (USENIX ATC’25) (July 2025). [49] Tasiran, S., Yu, Y., and Batson, B. Using a Formal Specification and a Model Checker to Monitor and Direct Simulation. In Proceedings of the 40th Annual Design Automation Conference (DAC’03) (June 2003). [50] Tu, H., Zhao, H., Song, Y., Zafar, M., Meng, R., and Roychoudhury, A. Agentic Verification of Software Systems. In Proceedings of the ACM International Conference on the Foundations of Software Engineering (FSE’26) (July 2026). [51] Wang, H., Zuo, X., Sun, Y., Li, Q., Ait Ameur, Y., and Dong, J. S. Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair. https://arxiv.org/abs/2605.17475, 2026. [52] Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.-C., and Tian, C. Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. In Computer Aided Verification (CAV’24) (July 2024). [53] Xia, C. S., Wei, Y., and Zhang, L. Automated Program Repair in the Era of Large Pre-trained Language Models. In Proceedings of the IEEE/ACM 45th International Conference on Software Engineering (ICSE’23) (May 2023), pp. 1482–1494. [54] Xu, Z., Jain, S., and Kankanhalli, M. Hallucination is Inevitable: An Innate Limitation of Large Language Models. https://arxiv.org/abs/ 2401.11817, 2024. [55] 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. Proc. ACM Program. Lang. (Oct. 2025). [56] Yang, F., Ma, X., Wang, S., Xu, X., Cao, Q., Zhan, N., Li, X., and Gu, B. Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications. https://arxiv.org/abs/2506.09550, 2026. [57] Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., and Zhou, L. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI’09) (Apr. 2009). [58] Yang, J., Jimenez, C. E., Wettig, A., Lieret, K., Yao, S., Narasimhan, K., and Press, O. SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering. In Proceedings of the 38th Conference on Neural Information Processing Systems (NeurIPS’24) (Dec. 2024). 16

Specula: Scaling formal specifications for autonomous model checking of system code [59] 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’99) (Sept. 1999).

17