LLMs are making formal software verification feasible at a much larger scale
anthropic.com
October 22, 2026
17 min read
66/100
Summary
Anthropic and formal-verification company Theorem used Claude to generate machine-checkable proofs for security properties in open-source software at the RISC-V assembly level. Over several weeks, Claude patched bugs and proved that 239 OSS-Fuzz entry points across 123 libraries would not crash for any input below 64 MB, under assumptions including a single-threaded static RISC-V binary, Linux, and a fixed memory budget. The proofs cover normal exits without assertion failures or modeled memory-safety errors, rather than proving that the libraries are entirely bug-free. The effort produced roughly 180 million lines of Rocq proof code, with a typical proof about 600,000 lines for a binary containing a median 18,000 RISC-V instructions. Claude found hundreds of bugs while attempting the proofs, including out-of-bounds reads and writes requiring unusual or large inputs, a rediscovery of CVE-2026-56132 in libexpat, and a logic flaw in a file-loading restriction feature. Anthropic is publishing a subset of the proofs, relevant RISC-V and Linux semantics, and specifications that it could not prove; Theorem plans to offer the pipeline for other open-source projects. The guarantees depend on the correctness and scope of the formal specification, processor and operating-system models, and the Rocq proof checker. The current proofs do not model common deployments such as x86 or ARM systems with dynamically linked glibc, and AddressSanitizer-based fuzz targets do not capture every possible vulnerability.
Key Takeaways
- Claude generated formally checked RISC-V binary-level proofs for 239 OSS-Fuzz entry points across 123 open-source libraries, covering inputs smaller than 64 MB under defined execution assumptions.
- Anthropic says the proof-generation process found hundreds of bugs, including rare input-dependent memory errors and a rediscovery of CVE-2026-56132 in libexpat.
- The project generated about 180 million lines of Rocq proofs, while the Rocq checker verifies the proofs without requiring developers to manually review all generated proof code.
- The proofs establish only stated properties, such as absence of modeled crashes and assertion failures; they do not establish that the affected libraries are completely bug-free.
- Anthropic reported that Opus 5.5 solved half of 36 small verification tasks using about 40% fewer tokens than Opus 5, while shared proof workspaces reduced agent token use by 17%.
What the discussion said
The thread treated the headline less as a triumphal claim about proof automation than as a question of where LLMs genuinely help formal methods. Several readers found the concrete workflow compelling: agents can generate machine-checked equivalence proofs, expose edge-case bugs, and make optimization experiments safer to merge. One practitioner described translating legacy C and replacement Rust into Lean and already checking tens of thousands of lines; others saw proof-backed SIMD, CUDA, VM, and bytecode-optimization work as evidence that this is becoming useful rather than merely academic. Proving properties directly over binaries or showing a fuzzer has no crashing input in a bounded space was seen as substantially stronger than collecting more random test cases. But enthusiasm was sharply bounded. Commenters stressed that a proof only establishes the property someone formalized, so errors can migrate into specifications, language/compiler models, hardware assumptions, or the theorem’s connection to the deployed program. They also doubted that today’s agents can scale their repetitive, execution-level proof style: without modular abstractions, proof contexts become too large and mechanical detail overwhelms them. A broader social skepticism ran through the thread as well: cheaper verification could improve critical systems, yet organizations may instead use AI to ship more unreviewed code faster. The likely near-term value is strongest in equivalence checking and narrowly specified security-critical behavior, not automatic validation of vague human intent.
Where opinion split
The central fight is whether LLM-assisted proof systems meaningfully raise software assurance or merely relocate mistakes into specifications and models. Supporters argue that machine-checked proofs can cover every input within a defined scope, surpass fuzzing and making safe refactors or optimizations practical. Skeptics answer that the decisive question is still whether the property, source-to-proof translation, compiler, and hardware model represent what users actually need, a problem no generated proof dissolves.
Coverage & discussions
Hacker News · anthropic.com
Community discussions
Community Sentiment
Positives
- LLM-generated proofs can turn equivalence checking into a practical guardrail for large rewrites, catching subtle behavioral drift across tens of thousands of legacy-code lines.
- Proving that no bounded machine-code input can trigger a crash goes far beyond a fuzzer’s sampled cases, making the technique especially attractive for vulnerability reduction.
- Proof-backed optimization proposals let teams explore SIMD or GPU speedups while retaining a formal behavioral link to the original implementation.
- Using AI to draft proofs and verification scaffolding could bring high-assurance techniques out of specialist niches and into ordinary systems work.
Concerns
- Agent proofs currently sprawl through register states, conversions, addresses, and stack contents; that brute-force style is likely to hit a complexity wall without better abstractions.
- A theorem can be impeccably checked while verifying the wrong thing, because flawed specifications, inaccurate semantic models, compiler defects, and hardware behavior sit outside its guarantee.
- LLMs often generate assumptions and tests only when explicitly prompted, undermining the hope that routine AI coding will naturally become verification-first.
- Cheaper code generation may push organizations toward more unvetted output rather than toward the discipline required to formalize meaningful properties.
