Correctness Too Cheap To Meter: Formal Verification and LLMs
summary
Argues that LLMs plus formal tooling can automate spec creation: a pipeline called Specula mines repos, generates TLA+ models, instruments code, runs TLC model checking and trace validation, and reproduces bugs. Reports 165+ bugs (134 previously unknown), average bug requires a 24‑action model check, false positive rate ~4.7%, run cost ≈€36 and ≈3 hours per repo. Baseline benchmark SysMoBench shows high syntax rates but poor conformance, so precise trace grounding remains the core challenge.
AI-written summary · about
chapters (25)
- 0:00Introduction to formal verification
- 1:12Why formal methods matter
- 2:16TLA+ and its workflow
- 3:41Low-level specs for real bugs
- 4:45How TLC detects violations
- 6:09Trace validation explained
- 7:52Manual effort in TLA+
- 8:57Can LLMs generate specs?
- 10:01Measuring spec quality
- 10:43System Bench results
- 12:27LLM progress and limits
- 13:52Enhancing agent workflow
- 15:18Specula pipeline overview
- 17:22Repository mining phase
- 18:04Spec generation and refinement
- 18:46Model checking and trace validation
- 19:49Bug reproduction and reporting
- 20:11Case study libgomp
- 21:55Production bugs found
- 23:18Cost and efficiency of Specula
- 24:22Limitations and false positives
- 25:44Specula’s real-world value
- 26:47Fighting AI slop with specs
- 27:30Future of automated verification
- 28:34Q&A session
related talks
23mUsing LLM Generated Formal Specs to Prevent the Next DeFi Hack
38mMaking LLMs reliable - A practical framework
47mHarnessing LLMs for Next-Level Security Analysis
01h 00mAI Safety through Programming?
32mThe Sorcerer’s Apprentice: The craft of building reliable solutions with LLMs
35mEvaluating LLM systems: the nuts and bolts
22mTowards Automated Verification of LLM-Synthesized C Programs
29mCustomizing and Evaluating LLMs, an Ops Perspective