Specula is an agentic system that automates formal specification and model checking to find concurrency bugs in system code, deriving TLA+ specs from code, git history, and issue trackers, then validating them via trace conformance and model checking. Run across 48 real-world distributed systems (MongoDB, SONiC, etcd, RabbitMQ, etc.) spanning 7 languages, it found 249 bugs, 207 new, in 1.4-9.8 hours at a median cost of $57 per system. A comparison against raw Claude Code and Claude Code with TLA+ tooling showed Specula's self-evolving loop of trace validation versus model checking vastly outperforms both (62 bugs vs 2 and 3 on five systems). The author, an academic and TLA+ Foundation member, praises the engineering achievement but raises deep concerns: since specs are derived from the same code being checked, there's a circularity problem where existing bugs could be baked in as 'intended' behavior; the protocol-level vs code-level invariant distinction meant to guard against reward-hacking is itself agent-determined and mostly (78.9%) code-level; convergence relies on an unproven assumption that agents improve over iterations; and the system doesn't handle compositional/cross-service verification, which is where the scariest distributed systems failures actually occur.
Table of contents
Why is Specula an Impressive AchievementThe Tautology Problem: How Do You Infer Intent From Buggy Code?Is This Smart Fuzzing with Inferred Specs?The Big PictureQuestions this post answers
How many bugs did Specula find compared to raw Claude Code and Claude Code with TLA+ MCP tools?
On five evaluated systems, Specula found 62 bugs, while raw Claude Code found only 2 and Claude Code equipped with official TLA+ skills and MCP servers found only 3. This indicates the improvement comes from Specula's self-evolving loop combining trace validation and model checking, not from simply giving an LLM TLA+ tooling or knowledge. Teams evaluating agentic bug-finding tools can track results like these on daily.dev before adopting them.
What happens to Specula's bug-finding performance when swapping Opus for a smaller model like Sonnet or Haiku?
Swapping Opus-4.8 for Sonnet-4.6 drops bug detection from 62 to 10 bugs found, at roughly similar wall-clock time and 61% of the cost. Swapping in Haiku-4.5 finds zero bugs and repeatedly declares the task complete prematurely; Haiku still writes 95% syntactically correct TLA+ but scores only 17% on invariant quality, showing the model's reasoning ability drives most of the results. Developers comparing LLM capabilities for agentic coding tasks can follow findings like this on daily.dev.
What is the circularity problem with deriving formal specifications directly from source code?
When a specification is derived from the same code, comments, and commit history that may contain the bug, there is no independent ground truth to check against, so bugs can get encoded as intended behavior rather than caught. Only 20% of Specula's invariants trace to documentation, versus 87% to code and comments and 74% to issue trackers, meaning the spec and code share the same flawed source most of the time. Engineers weighing AI-driven spec generation against traditional formal methods can dig into debates like this on daily.dev.
2.2K Impressions1 Comment