Weekly Paper Notes — one of the top picks from the 2026-08-01 CS paper digest. Area: Operating Systems / Formal Methods.
Authors: Qian Cheng, Ruize Tang, Yu Huang (Nanjing University); Saad Mohammad Rafid Pial, Yiming Su, Tianyin Xu (University of Illinois Urbana-Champaign); Emilie Ma, Finn Hackett, Ivan Beschastnikh (University of British Columbia)
arXiv: 2607.25333 · PDF · Code
TL;DR
Formal verification of real systems has always been bottlenecked by the same thing: writing a good TLA+ specification takes a domain expert months, and the specification immediately begins drifting away from the code it describes. Specula is a push-button agentic system that removes the human from that loop entirely. It points LLM-based coding agents (Claude Code, Codex, Copilot CLI) at a system repository, has them infer both the invariants the system must uphold and a TLA+ model of the implementation at an abstraction level chosen to make model checking tractable, then validates that model against real execution traces harvested from instrumented code. Every invariant violation TLC reports is replayed at the code level and wrapped in a reproducible test. The authors ran Specula over 48 open-source projects — MongoDB, Etcd, ScyllaDB, GCC’s libgomp, LLVM’s libomp among them — and found 249 bugs, 207 of them previously unknown, with no false positives, because every reported bug is reproduced against the real binary. 89 were reported upstream; 68 confirmed and 24 already fixed. The system is open source and, per the paper, already in use at several companies.
What problem is the paper actually attacking?
The lineage here is long and the failure mode is well documented. TLA+ has been used at scale in industry since the Amazon experience reports of the mid-2010s, and the pattern in every one of those reports is identical: a small number of exceptionally skilled engineers write a specification of a protocol, find real design bugs, and then the specification sits in a repository slowly becoming a lie as the implementation evolves underneath it. This is the classic model–code gap. A specification that describes the protocol you designed tells you nothing about the C++ you actually shipped.
The research response has been trace validation: instrument the running system, collect execution traces, and check whether those traces correspond to legal paths through the model’s state space. That works, but it only reduces the maintenance burden — someone still has to write the model, and writing a model requires simultaneously mastering the system’s implementation and TLA+’s toolchain. The authors are blunt that their own prior efforts were “limited to specific system projects and are hard to scale.”
So the obvious move in 2026 is: point a coding agent at it. And the paper is admirably clear about why the obvious move fails. Three specific failure modes:
- Context exhaustion and hallucination. A large system’s codebase exceeds what an agent can hold in context. Agents respond by hallucinating execution paths, oversimplifying concurrency, and — most insidiously — falling back on the canonical TLA+ models they memorised during pretraining. You ask for a model of ScyllaDB’s Raft and get a model of the Raft paper, which is precisely the model–code gap you were trying to eliminate.
- No basis for choosing an abstraction level. Too abstract and the model can’t find code-level bugs; too concrete and TLC drowns in state-space explosion. Human experts pick this level by intuition and experience. Agents have no such prior.
- Reward hacking. If you reward an agent for making trace validation pass, it will weaken the invariants until they pass. This is the killer. A specification that has been quietly relaxed until it’s trivially satisfiable is worse than no specification, because it carries a badge of formal rigour.
The single observation that motivates Specula’s design is that generation is now cheap but correctness is not. A frontier agent can emit syntactically valid, plausible-looking TLA+ in seconds. What it cannot do is know whether that TLA+ means anything. So the design problem shifts entirely away from generation and toward building a harness that can tell good specifications from bad ones without a human in the loop.
The mechanism: self-evolving loops with opposing pressures
Specula’s core trick is to pin the agent between two forces that pull in opposite directions, so that reward hacking in either direction is caught by the other.
- Trace validation ensures the model is permissive enough: every behaviour the real code exhibits must correspond to a legal path in the model. An agent that over-abstracts fails here.
- Model checking against invariants ensures the model is restrictive enough: the model must not admit states that violate the correctness properties. An agent that weakens the model to pass trace validation gets caught here.
Neither check alone is sufficient, and — critically — an agent cannot satisfy both by cheating, because the cheats are in opposite directions. This is the “clear boundaries” the paper refers to when it describes preventing reward hacking.
Invariants themselves come in two flavours, and the distinction matters. Protocol-level invariants are the textbook properties — for Etcd-Raft, Specula generates the classic durability property:
\* Any committed entry is on a majority's durable storage
CommittedInDurableStorage ==
\A s \in Server :
commitIndex[s] <= durable_storage[s]
Code-level invariants are inferred from the artefacts around the code — test cases, issue trackers, revision histories — and describe properties the implementation upholds that the protocol never mentions. For MongoDB:
\* Any committed entry is on a majority's log (in memory)
CommittedInLog ==
\A s \in Server :
commitIndex[s] <= Len(log[s])
That second class is where the deep bugs live, because nobody has ever written those properties down. Specula mines them from commit history: the paper shows an example where three separate historical fixes to joint-configuration voter tracking in ScyllaDB become evidence for a ReadBarrierProgress liveness invariant, which then becomes a scenario-specific model.
The abstraction-level problem is solved by inverting the dependency: rather than picking an abstraction and hoping it finds bugs, Specula lets the inferred invariants drive the modelling. Behaviours irrelevant to a given correctness property get abstracted away; behaviours the property depends on get modelled in detail. Because generation is cheap, the system produces multiple models of the same system at different abstraction levels, one per class of invariant. This is the paper’s sharpest idea: model customisation was previously an expensive expert judgement call, so you got one model. When models cost seconds, you get a family of scenario-specific models, each tuned to the state space where a particular bug class hides.
Why this doesn’t drown in state-space explosion
The scenario-based projection is the answer. Specula maintains a reference model of the target system and projects it down to customised models for the specific scenarios it has generated from evidence. Instead of one monolithic model that must be simultaneously detailed enough to find concurrency bugs and small enough for TLC to explore, you get many narrow models, each cheap to check.
The other practical concern is soundness of the reports, and Specula’s answer is aggressive: no violation escapes as a bug report unless it has been replayed at the code level. When TLC produces a counterexample, the model-level trace is used to drive a code-level replay, and the result is packaged as a system test. This is why the paper can claim zero false positives across 249 findings — a claim that would be extraordinary for a static analyser and is only credible here because the final filter is actual execution.
It also means the reproduction step doubles as a third pressure in the evolving loop. If a violation cannot be reproduced, that is itself evidence that either the model or the invariant is wrong, and the loop iterates. The paper is careful to argue this is safe: invariant revision requires the agent to supply strong evidence that the original invariant was incorrect, and it is explicitly not permitted as a way to make a violation go away.
Results
The headline number: 249 bugs across 48 systems, spanning seven categories, covering both distributed systems (MongoDB, Etcd, ScyllaDB) and concurrent systems (GCC libgomp, LLVM libomp). Of these, 207 were new and 42 were rediscoveries of known issues — a healthy ratio that suggests the technique isn’t merely re-finding what regression suites already cover. 200 of the 249 (80.3%) surfaced through the mechanisms Specula adds on top of raw agent generation, rather than from first-pass output.
The disclosure numbers are the ones that matter for credibility: 89 bugs reported upstream, 68 confirmed by maintainers, 24 already fixed at time of writing. Maintainer confirmation is a much harder currency than a self-reported bug count.
The ablation against Agent-TLA+ — essentially “just ask a coding agent for a TLA+ spec” — is the comparison that justifies the whole architecture. Agent-TLA+ has no model–code conformance mechanism and no self-evolving loop, and the paper’s evaluation of loop effectiveness concludes the loops are essential, not incremental. Elsewhere the authors note that the latest Specula reported 136 findings in a configuration where the ablated pipeline produced far fewer usable results. The SONiC module study is a nice sanity check on breadth: Specula surfaced at least one bug in each module it was pointed at.
Configuration detail worth noting for anyone reproducing: the default is Claude Code with Opus-4.8, but the harness is agent-agnostic and also supports Codex and Copilot CLI. Since Specula abstracts the implementation into TLA+, it is likewise programming-language-agnostic — the C++, Go and Java systems in the evaluation all go through the same pipeline.
Why this matters
For twenty years the honest answer to “should we formally specify this system?” has been “only if it’s Paxos-shaped and you have a Lamport-adjacent engineer with six spare months.” Specula’s claim is that the cost side of that calculation has collapsed, and the paper’s evidence is 249 reproducible bugs in production infrastructure people actually run.
The deeper contribution is architectural, and it generalises well beyond TLA+. The pattern is: when generation becomes free, invest everything in the verification harness, and make sure the harness applies opposing pressures so the generator cannot satisfy it by degradation. Trace validation says “your model must admit reality”; model checking says “your model must reject invalidity”; code-level reproduction says “and your bug must actually happen.” An agent optimising against any one of these will be caught by the others. That triangulation is a transferable design principle for any agentic system where the output is expensive to verify and cheap to fake.
The obvious follow-up is liveness at scale — the paper touches on liveness invariants but the bulk of the harvest is safety — and extending the projection technique to symbolic model checking via Apalache, which would push the tractable state-space frontier considerably further out.
Read alongside
- Lamport, Specifying Systems (2002) — the canonical TLA+ reference; the language and TLC model checker Specula automates.
- Newcombe et al., “How Amazon Web Services Uses Formal Methods” (CACM 2015) — the industrial experience report that established both the value and the human cost this paper is attacking.
- Yu, Manolios & Lamport, “Model Checking TLA+ Specifications” (1999) — the TLC explicit-state checker at Specula’s core.
- Konnov et al., “Apalache” — symbolic model checking for TLA+; the natural scaling path beyond TLC.
- Ongaro & Ousterhout, “In Search of an Understandable Consensus Algorithm” (2014) — Raft, the protocol whose implementations (Etcd, ScyllaDB) supply most of the paper’s worked examples.
- Davis et al., “Extreme Modelling in Practice” (VLDB 2020) — trace validation against real system executions, the technique Specula automates.
Links
📄 arXiv abstract · 📄 PDF · 💾 code
Part of the Weekly CS Paper Digest series. Summary written from a close read of the preprint; figures cropped from the arXiv PDF and reproduced here under fair use for educational commentary.