formal verification at scale via agents
Specula agents auto-generate TLA+ specs, find 130+ unknown bugs across 47 open-source projects Plain Schwarz (Berlin Buzzwords, Haystack)TL;DW
- Specula automatically generates TLA+ specifications from code using agents, discovering 130+ previously unknown bugs in production systems like MongoDB and Raft with 4.7% false positive rate.
- TLA+ specs require separate modeling from code and multi-month engineering effort; Specula automates this workflow for ~$36-40 per project, making formal verification economically feasible at scale.
- LLMs alone score poorly on spec generation (especially conformance and invariance metrics at ~30-40%), but agents equipped with TLC model checking, trace validation, code instrumentation, and step-through debugging achieve 100% on key quality metrics.
- Specula's four-phase pipeline: repository mining (identifies suspicious modules via code churn heuristics), spec generation with syntax validation, model checking and trace validation (automated debugging that took 2 engineer-months manually), and bug reproduction with evidence.
- Discovered bugs require average 24 sequential actions to trigger, explaining why manual testing missed them; formal methods' exhaustive state exploration catches complex interleaving bugs humans cannot find.
- Trace validation maps real execution logs to abstract TLA+ actions, catching specs that don't match implementation; critical because specs useless if they don't reflect actual code behavior.
- Agent tools should include GitHub issues, git commits, code comments, and execution traces—context humans use but LLMs lack by default—to ground generated specs in reality and reduce hallucinations.
- Tool provides rigor for AI-generated code verification: instead of manually reviewing hundreds of thousands of lines, developers examine formally model-checked invariants, creating virtuous cycle of software correctness.
- Specula found bugs across 47 systems including serious issues: deadlocks, data corruption, memory safety errors (even in Rust), with C/Erlang/Java projects showing higher bug rates than Go/Rust.
- 15% of codebase remains unverified by traces; false positives stem from undocumented developer assumptions; affordable formal verification adoption now feasible, shifting from human-effort constraint to cost-efficient automated verification.
TL;DW
- Specula automatically generates TLA+ specifications from code using agents, discovering 130+ previously unknown bugs in production systems like MongoDB and Raft with 4.7% false positive rate.
- TLA+ specs require separate modeling from code and multi-month engineering effort; Specula automates this workflow for ~$36-40 per project, making formal verification economically feasible at scale.
- LLMs alone score poorly on spec generation (especially conformance and invariance metrics at ~30-40%), but agents equipped with TLC model checking, trace validation, code instrumentation, and step-through debugging achieve 100% on key quality metrics.
- Specula's four-phase pipeline: repository mining (identifies suspicious modules via code churn heuristics), spec generation with syntax validation, model checking and trace validation (automated debugging that took 2 engineer-months manually), and bug reproduction with evidence.
- Discovered bugs require average 24 sequential actions to trigger, explaining why manual testing missed them; formal methods' exhaustive state exploration catches complex interleaving bugs humans cannot find.
- Trace validation maps real execution logs to abstract TLA+ actions, catching specs that don't match implementation; critical because specs useless if they don't reflect actual code behavior.
- Agent tools should include GitHub issues, git commits, code comments, and execution traces—context humans use but LLMs lack by default—to ground generated specs in reality and reduce hallucinations.
- Tool provides rigor for AI-generated code verification: instead of manually reviewing hundreds of thousands of lines, developers examine formally model-checked invariants, creating virtuous cycle of software correctness.
- Specula found bugs across 47 systems including serious issues: deadlocks, data corruption, memory safety errors (even in Rust), with C/Erlang/Java projects showing higher bug rates than Go/Rust.
- 15% of codebase remains unverified by traces; false positives stem from undocumented developer assumptions; affordable formal verification adoption now feasible, shifting from human-effort constraint to cost-efficient automated verification.
Emily Ma's Specula pipeline chains LLM agents with repository mining, syntax validation, and model-checking tools across four phases to produce TLA+ specs without manual effort. Evaluated on MongoDB, HashiCorp Raft, ZooKeeper, and others: 95.3% maintainer-confirmed bug rate at ~€38 and 3 hours per project.