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

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. 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. 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. 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 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. 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? 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 a separate requirements spec, and separate code. For formal methods people, writing the specification IS understanding the problem; the code is the easy part afterwards. Specula runs that backwards: the code is the given, and the understanding is reconstructed from it. But then the word "specification" is doing something different than it does in Lamport's world (i.e., formal methods and mathematics), and the paper never talks about this. This is also where the vocabulary starts sliding. In the conformance loop the paper considers three cases: the model/spec is incorrect, the code has a bug, or the invariant is incorrect. Incorrect with respect to what?? For the model/spec, the answer is with respect to the code, and for the code the answer is with respect to the model/spec. Notice the circularity? For the invariant, there is no external reference point at all! The invariant is incorrect with respect to the agent's own reading of the artifacts, revised by the agent, justified by evidence the agent selects. The practical answer the paper offers, as far as I can tell, is that specification will identify a bug when the artifacts disagree with each other. Specula's scenario generation tries to catch these disaggrements. But, if the design is wrong and everybody wrote it down consistently, there is nothing to catch. If the agent misreads an ambiguous comment in the other direction, it would quietly relax a real invariant to match a code flaw, and you never hear about it. Is This Smart Fuzzing with Inferred Specs? They ran all of this on an Azure VM with a 96-core AMD EPYC 9V74 and 384GB of RAM, driving Claude Code with Opus-4.8 at a 1M context and max reasoning. And even with that machine, Specula does not model check the full reference specification, because it would blow up the state space. Instead, it projects things down to the aforementioned per-scenario models with some tricks: bound how many times an action can fire, (e.g., bound=0 for a crash action means happy path checking), coarsen multi-step processes into one atomic action, and serialize action pairs into a fixed order. Every one of these is a legitimate technique, and human modelers use all three. What bothers me is that none of it is justified. Why these three operations? Coarsening an action is only sound for properties that do not observe the intermediate states, so which invariants survive which coarsening? The paper says intermediate states are abstracted out and moves on. When a human expert makes that call they have a justification in mind. I am not sure about agents trying these in an automated way. It sounds more ad hoc, as a means for smart fuzzing the system. The protocol-level versus code-level split has the same feel, and I think it is more critical because it is load-bearing. The whole anti-reward-hacking argument depends on protocol-level invariants being independent of the code the agent just modeled. The paper gives example: Etcd-Raft gets "committed entries are on durable storage," but MongoDB gets the weaker "an entry is in the server's own log before it is reported committed," because MongoDB deliberately deviates from Raft to cut write latency, and the agent digs that out of the revision history. Nice. So protocol-level means it holds for any conforming implementation, and code-level means it is what this implementation promises. Except only 21.1% of Specula's invariants are protocol-level. The other 78.9% are code-level, mined from the same artifacts as the model. So the guard against overfitting rests on a fifth of the invariants, and the agent is the one who decides which fifth, and nothing checks that call. Misclassify a description of the current code as a protocol-level invariant, and you are now guarding against reward hacking using a reward-hacked artifact. This is in essence a sharper version of my complaint about spec from code being circular. What worries me further is by looking at Fig 3.a and 3.b, I don't see any structural or qualitative difference between the two invariant types, so the distinction seems more ad hoc and easy to blur/confuse. Then there is the convergence issue. The paper says the evolving loops are safe and that Specula "offers convergence with the assumption that agents improve over the iterations". That is not assuring because the assumption does all the work. The stated failure mode of a bad invariant is that the process just does not converge and keeps iterating, and in practice you stop it with a time or token budget. Their numbers are better than I expected, all recorded runs converged, instrumentation fixed within three rounds, 91.3% of invariant and model errors fixed in one iteration, none over four. The one case that needed four rounds was SONiC's link manager. The agent wrote an invariant saying a link's two gateways are never both on standby. Model checking kept finding states where they both are: a failover in mid-handoff, or a degraded mode where neither gateway can take over. Those states are legal, just temporary. It took four counterexamples before the agent stopped calling them bugs and fixed its invariant instead. So the self-evolving loop worked once again. But, this also shows how hard it is to tell a real bug from a state that only looks broken. I mean it is all pragmatic, which is fine. But I am really bugged by lack of principled justification for these. And the ad hocness of their introduction/descriptions in the paper. Maybe this is the new science we are doing... A more heuristic type of computer science with a mix of anthropology (well, study of agents, so agentology). Maybe in the future, the paper's will consists mostly of field notes on how agents misbehave and which guardrails stop them. No denying to it, Opus does a lot of the heavy lifting in Specula, and the authors are upfront about it. Swap in Sonnet-4.6 and Specula finds only 10 of those 62 bugs, at nearly the same wall clock and 61% of the cost, so$ 59 per bug instead of $16. Swap in Haiku-4.5 and it finds nothing at all, and keeps declaring the task done before it is done. The gap shows up in the spec-quality scores: Haiku still writes 95% correct TLA+ syntax, but scores 17% on invariants. But look at how fast that part moved. When I reviewed SysMoBench, the benchmark from this same group (which came on Jan 2026), the authors had handed LLMs invariant templates and asked it only to map them onto its own variable names, because invariants are the most signal-heavy part of a spec. Specula now has agents deriving invariants from commit history unaided. The Big Picture Specula is a great pragmatic idea, and it works for what it does. My critiques are mostly about naming the contributions/mechanisms more precisely, plus a last ditch effort to get the ad hocness out of the methods. And I should be honest about where that effort is coming from. When we get around to writing our own paper on agentic specification-based development, I am certain we will reach for the same kind of heuristics, and I will find myself defending them with the same hand-waving I am complaining about here. That is what is really bugging me. I do not know what the non-ad-hoc version of this paper would even look like. All this being said, there is still plenty is to address even on the pragmatic front, because Specula skirts the real hard problem: composition. Specula steers away from authoring and reasoning with compositional specs for multi-service codebases. There is no compositional verification or assume-guarantee reasoning employed when writing specs, as they are monolithic cross-slices of a system. For a system with multiple services, like SONiC's 5 distinct daemons, Specula builds one model per module and mocks the cross-service interactions inside the scenario models. So it cannot say anything about whether the per-module guarantees add up to a system-level guarantee. Unfortunately, the failures you actually fear in distributed systems are the cross-boundary ones , especially for recovery related failures. PS1 : TLA+ for the win!! I got so wrapped up in my own thinking around Specula that I forgot to pat TLA+ on the back. Full disclosure, I am part of the TLA+ Foundation , which recognized and provided some funding for Specula. It is a great addition to the TLA+ ecosystem, and you should go try it: https://github.com/specula-org/Specula PS2 : Here is the link to my marked up copy of the paper. Even with the availability of LLMs, I still believe in deep manual reading , and illustrating one's thought-processes to teach/train others.