arxiv-2607.25333-specula

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

URL: https://arxiv.org/html/2607.25333v1 (also abs https://arxiv.org/abs/2607.25333; html v2 exists)
Fetched: 2026-09-27 ~19:34 CST · defuddle parse —md (html) + abs metadata
Authors: Qian Cheng (NJU), Saad Mohammad Rafid Pial (UIUC), Ruize Tang (MSR Asia), Yiming Su (UIUC), Emilie Ma, Finn Hackett, Ivan Beschastnikh (UBC), Yu Huang (NJU), Tianyin Xu (UIUC)
Code: https://github.com/specula-org/Specula · ~5.5K LoC Markdown Agent Skills + 24.8K LoC Python/shell/Java orchestration
Stack: TLA+ models + TLC (BFS + simulation); coding agents (default Claude Code + Opus-4.8; also Codex, Copilot CLI); automated instrumentation + trace validation; self-evolving repair loops

Push-button agentic TLA+: agents autonomously produce (1) invariants (protocol-level + code-level) and (2) formal models at the right abstraction, then model-check for bugs — language-agnostic (models abstract C/C++/Go/Java/Rust/…).
Addresses LLM reward-hacking/hallucination via self-evolving loops + bidirectional grounding: trace validation (model must admit code traces) paired with model checking (reject illegal states / overfitted repairs).
Scenario-based projection of a reference model (select/bound actions, coarsen, serialize) keeps state spaces tractable while preserving that scenario violations lift to the reference model.
Bug reproduction is controlled schedule replay (client APIs → sleeps → preconditions → in-code sleeps); forbids reward-hack shortcuts (preload illegal state, call private fns, change logic).
Framing important for DIY: Specula is model-checking / bugfinding on code-grounded specs, not product-level theorem proving of the implementation.

48 OSS projects (36 distributed + 12 concurrency; 7 languages; 2K–95K LoC) → 249 bugs (207 new, 42 known-unfixed). Reported 89; 68 confirmed, 24 fixed. Authors claim no false positives (all reproduced at code level).
Of 249: 200 (80.3%) via model checking (187 BFS shortest CEx, median length 9 / p90 18; 13 via random simulation); rest during comprehension/modeling.
Invariants: 99.1% safety / 0.9% liveness; 21.1% protocol-level / 78.9% code-level.
Latest Specula (14 shaded systems): 136 bugs; 134 encapsulated in tests; 2 reproduced but masked.
Cost: 1.43–9.86 h / system (median 3.69 h); $19–$ 168 tokens (median $57). Vs Agent-Raw / Agent-TLA+ on 5 systems: Specula ~4.8–37× / 1.8–65× more expensive but perfect SysMoBench scores + 0 FP (others had FPs from bad specs on libspdm).
Self-evolving: all runs converged; instrumentation ≤3 rounds; 91.3% invariant/model errors fixed in 1 iter (max 4). Agent sensitivity: Sonnet-4.6 finds 10/62 of Opus-4.8 bugs; Haiku-4.5 finds 0.
Case: libgomp fast-barrier patch — 6 h compute + 1.5 h human review → 2 bugs (one new, one latent ≥5 years deadlock).

Harness shape: artifacts → evidence-backed invariants (+ fault model) → reference model → scenario projections → instrument → TLC replay harness → bidirectional repair → TLC BFS/sim → reproduce as test.
Adopt: TLA+/TLC as DIY concurrent/distributed gate; evidence-required invariant lineage; scenario projection to fight state explosion; pair trace-val + MC against reward-hack overfitting; structured reproduction phases; skills-as-Markdown for agent orchestration.
Skip/caveat: treat “no FP” as reproduced-at-code claim, not unbounded FV; model ≠ runtime (aligns with Cherny/Runtime Verification framing in brief queue); cost & frontier-LLM dependent; skills compensate current agent weaknesses and will need retuning.
Related-work contrast: Specula = system-level behaviors vs BMC-Agent/FM-Agent function-level CBMC/Hoare.

Many Table-1 rows from early Specula versions (budget-limited rerun). Abs/html v1 parsed; v2 exists with same abstract. Confidence high on architecture and DIY patterns; medium-high on absolute 249 (mix of versions, developer confirmation 68/89 of reported).