Specula: Scaling formal specifications for autonomous model checking of system code
Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang, Yiming Su, Emilie Ma, Finn Hackett, Ivan Beschastnikh, Yu Huang, Tianyin Xu
cs.SE, cs.AI, cs.DC, cs.OS
2026-07-28
Specula lets LLM coding agents autonomously write TLA+ specs and model-check system code, finding 249 bugs in 48 open-source projects at a median cost of $57 per system.
Formal verification is the gold standard for finding deep concurrency bugs in system code. TLA+, Leslie Lamport's specification language, describes precisely how a system's state evolves, and a model checker then walks every possible execution to see whether it violates a correctness property. etcd, MongoDB, and ZooKeeper have all used it to surface defects no other method catches.
It never scaled. Writing a usable TLA+ spec for a real system used to take months and demanded three scarce skills at once: deep knowledge of the system, fluency in TLA+ and its toolchain, and ongoing effort to keep spec and code consistent. So it stayed confined to a handful of flagship systems.
Naively adding an LLM does not work either. Real codebases overflow an agent's context window, forcing imprecise models. Agents have no reliable basis for choosing the right level of abstraction. And reward hacking bites: an agent can quietly weaken an invariant so that the check passes on its own, rather than the model being correct.
Specula is push-button: hand it a repo and it produces TLA+ specs and finds bugs. The core is two self-evolving loops aimed squarely at those two failure modes.
First, understand correctness. The agent derives invariants from two sources: protocol-level (from protocol descriptions and docs) and code-level (from tests, issues, commit history). Each must cite concrete evidence from the code or artifacts.
Then build models. The agent reads code to produce a reference model, with the abstraction level driven by the correctness properties. The key design choice is that it does not build one giant model; it builds a set of scenario-based projections of the reference model, trimmed with three operations: enable only the actions a scenario needs, collapse a multi-step process into one atomic action, and constrain actions to a particular execution phase. Each model stays small enough to check exhaustively.
Next, model-code conformance. Specula auto-instruments the code to record execution traces, replays them against the TLA+ model, and confirms that every behavior the code can produce is admitted by the model. This is what stops the model from drifting from the code. It pairs with model checking as a two-way check: trace validation ensures the model permits the code's real behaviors, and model checking ensures it does not permit illegal ones. One direction alone is gameable; together, an overfit repair shows up immediately as a violation of the protocol-level invariant.
Finally, TLC runs in breadth-first mode (exhaustive up to a depth bound) and simulation mode to find violations. When one appears, reproduction at the code level proceeds in four phases: drive the client API, insert sleeps between calls for external concurrency control, construct preconditions on system state, and insert sleeps in the code for internal concurrency control.
Two self-evolving loops tie this together. In the conformance loop, when a repaired model fails the protocol-level invariant, the agent reasons about three cases: the model is still wrong, so keep repairing; it is a real bug, so reproduce it; or the invariant itself is wrong, so fix it and redo modeling. In the reproduction loop, a failure to reproduce restarts the conformance loop with the diverging state. Each iteration hands the agent new information (a counterexample, a model-code gap, a failed reproduction), forcing deeper understanding rather than gaming the checker.
Across 48 open-source systems (36 distributed, 12 concurrent), Specula found 249 bugs, of which 207 were new. 89 were reported, 68 confirmed, 24 fixed.
| Metric | Number |
| Bug source | Model checking found 200 (80.3%); BFS found 187 of those (93.5%) |
| Counterexample length | Median 9 steps, p90 18 steps |
| Bug type | Safety 99.1%, liveness 0.9% |
| Cost per system | $19 to $168, median $57 |
| Time per system | 1.43 to 9.86 hours, median 3.69 hours |
On 5 systems it compared against two baselines: a raw agent (Agent-Raw) found 2 bugs with 5 false positives, and an agent given TLA+ background (Agent-TLA+) found 3 with 2 false positives. Specula found 62 with zero false positives and scored 100 on SysMoBench, the spec-quality benchmark the authors built, against 81 and 82 for the baselines.
The bugs found are deep concurrency defects that testing and code review miss. In GCC's libgomp, a fast barrier path drops the BARCANCELLED flag and splits the barrier, and a wake path omits settaskpending, a deadlock latent for over five years. In HashiCorp Raft, a leader with a stalled disk keeps sending heartbeats that suppress elections, so the cluster can neither commit nor fail over. In MongoDB, the sharding module marks the wrong migration task ready and deletes the wrong data.
It pushes formal verification from "months of expert effort for one system" toward "hours, push-button, tens of dollars per system." For anyone running a distributed or concurrent system, that means a verification method once affordable only for the etcd tier has dropped steeply in cost.
It also clarifies where LLM agents add value over people: not by replacing expert reasoning, but by taking over the tedious, iterative, evidence-cited work of writing specs, instrumenting code, running trace validation, and repairing the model against counterexamples. Humans find that work expensive; agents find it cheap.
Zero false positives matters more than the bug count. The whole value of formal verification is that a violation is real; add false positives and it degrades into ordinary lint. The self-evolving loop plus bidirectional checking is what protects that property.
Cost is low in absolute terms but 4.8 to 37 times a raw agent and 1.8 to 65 times a TLA+-backgrounded agent. Cheap against months of human effort, expensive against other agent routes.
Some bugs could not be reproduced at the code level; the authors attribute this to a need for "external control." Trace validation is incomplete, so rare cases of model-code drift may slip through. Full runs take hours. Token cost tracks complexity rather than size, so very complex systems could blow up.
Liveness bugs are nearly absent (0.9%); the breadth-first plus simulation search favors safety, and there may be a blind spot here.
The comparison is only against other agent routes, not against the full human-expert TLA+ process, which costs far more but might surface different deep bugs. And the authors built both Specula and SysMoBench, the benchmark on which it scores 100, so that score needs independent confirmation.