Claude proves security properties for 123 open-source libraries using RISC‑V verification
The authors report that, in collaboration with Theorem, Claude was used to generate formal proofs for 123 open‑source libraries compiled to RISC‑V binaries. Over 239 entry points from Google’s OSS‑Fuzz initiative were proved never to crash for any input under 64 MB, and the process uncovered several long‑standing bugs, including an out‑of‑bounds write that required a 20 MB input and a…
Key points
- Claude generated about 180 million lines of Rocq proofs, with typical proofs around 600 k lines for libraries of median 18 k RISC‑V instructions.
- The pipeline proved 239 entry points across 123 OSS‑Fuzz libraries never crash for inputs under 64 MB, uncovering several long‑standing bugs.
- Agents sharing proofs used 17 % fewer tokens, and Opus 5.5 needed about 40 % fewer tokens than Opus 5 on 36 verification tasks.
The proofs total about 180 million lines of Rocq code, with a typical proof around 600 k lines covering binaries of median length 18 k RISC‑V instructions. The authors note that agents sharing proofs needed 17 % fewer tokens, and that Opus 5.5 required about 40 % fewer tokens than Opus 5 on 36 small verification tasks. They also measured 1.7 million randomly generated Python programs against a Rust interpreter and found 99.95 % behavioral agreement.
The paper concludes that as LLMs become more capable, formal verification could become as routine as fuzz testing for production software, provided the underlying machine models are refined.
LLMs are making formal software verification feasible at a much larger scale
anthropic.com · 22 October 2026
Loading the full article…
This text was published by anthropic.com and written by Anthropic. It is reproduced here with attribution so you can read it in full; the rights remain with the publisher. Read it at the source ↗
Coverage and discussion
1source- Hacker News discussion · 41 pointsnews.ycombinator.com
The headline, key points and digest above were generated by Digest AI's editorial model from the linked sources. Automated summaries can contain errors: the sources are the record. Spotted a mistake? Tell us. Published by Martin K., who runs Digest AI and handles corrections.
More in Research
All →- MIT researchers say AI agents play on virtual island after 30 hours · 1 src
- Anthropic offers $5M in grants for AI well-being research · 1 src
- PHP discloses critical PHP2Shell vulnerability affecting 70% of websites, discovered using GPT-5.6 Sol · 27 src
- John L. Hennessy and Eric Horvitz to headline Rice's Ken Kennedy Institute 40th anniversary · 1 src
- UCLA researchers develop maestro AI system to find prostate cancer drug combos · 1 src
Comments
via GitHub Discussions