Specula: Scaling formal specifications for autonomous model checking of system code
Skip to main content
Specula: Scaling formal specifications for autonomous model checking of system code
Get link
Other Apps
August 12, 2026
Specula is an agentic system that automates the process of software bug finding through authoring and model-checking a spec for the code. It derives TLA+ specifications automatically from the code, checks code-spec conformance through trace validation, model checks the spec to find concurrency bugs, and reproduces the bug at the code layer by writing integration tests with precise timing.<br>I remember reading the Daikon paper "Quickly detecting relevant program invariants" in 2000 and getting impressed by it, and here we are after 26 years, solving the end-to-end problem much better than I ever thought would be possible in a push-button manner in the year of our lord 2026.<br>But somehow, I am still somewhat unsatisfied with the paper. This may be me being hypercritical and trying to get more out of the paper by arguing with it. So bare with me until I resolve (or learn to accept) these problems over time. I know many of the authors of the Specula work, and respect them, and I know they won't take my critiques about the larger problem in a wrong way... I am trying to make sense of the terrain myself.<br>So, let's look at what Specula gets right, its major contributions, and then dive into my unresolved questions and existential thinking about the terrain.
Why is Specula an Impressive Achievement<br>Specula is run on "slices of" 48 complex open-source distributed and concurrent systems including MongoDB, Microsoft's SONiC network OS, GCC's libgomp, Etcd, and RabbitMQ's ra. It found 249 bugs, 207 of them new. The 48 systems span 7 languages, from C to Erlang to Rust. This is very impressive, and it earns the "scaling" claim in the title of the paper. Hand-crafting TLA+ specifications may take weeks (especially for unfamiliar code bases), and Specula completes end-to-end checks in 1.4 to 9.8 hours at a median token cost of $57 per system. Did I mention this is all push-button? Developers just review the end results. They may not even have to look at the TLA+ specs, and they may just check the reported bugs and figure out how to address them.
OK, impressive. Let's dive into the technical novelty here. As far as I understand the technical novelty arises from two opposing forces dueling it out in self-evolving loops, to achieve an "iron sharpens iron" effect. Trace validation pulls the spec toward the code, and model checking pushes back. You need the two opposing forces, because either one alone gets fooled. Left with only trace validation as its reward signal, the agent does reward-hacking: it relaxes guards in the spec, adds wildcards, hardcodes trace-specific updates just to make the log replay. For example, in the Kudu-Raft application, the agent "repairs" the follower's accept path so it overwrites the log suffix unconditionally, and the traces replay beautifully, and then State Machine Safety catches the problem in one step. The model checking checks that the spec/model has nothing illegal in it. Specula wires them into self-evolving loops where each iteration hands the agent new evidence, a counterexample, a model-code gap, a failed reproduction, and forces it to reconsider. In short, these loops turn an unreliable agent into a reliable one.
To evaluate this technical novelty, they ran the same prompts three ways: Claude Code raw, Claude Code with the official TLA+ skills and MCP servers, and Specula. On five systems, Specula finds 62 bugs, raw finds 2, and TLA+-equipped finds only 3. So handing a frontier agent the entire TLA+ toolchain doesn't buy you much, and Specula leaves that baseline in the dust. As the authors put it, what is lacking is not TLA+ knowledge, it is the runtime feedback that lets the agent repair what it wrote. I think that large gap in the evaluation highlights that the technical contribution of Specula is not prompting/hyping LLMs, and is not just handing the LLM a model checker.<br>But, my problem is that I cannot put my finger on the technical contribution in a very robust/solid/concrete sense. The technical contribution seems to be, so to speak, self-emerging from a set of (somewhat unsound) heuristics . Let me try to explain...
The Tautology Problem: How Do You Infer Intent From Buggy Code?<br>Specula treats system artifacts (code, git commit history, PRs, comments) as the ground truth to derive invariants. 87% of its invariants trace back to the implementation code and comments, 74% to issue trackers, and only 20% to documentation. So the specification derivation sources from the code, the same place the bugs live. So how does Specula find bugs if it treats the codebase as the ground truth? Wouldn't it just copy existing bugs into the model as intended behavior? What stops this?
Leslie Lamport will never understand this... You need...