# Anthropic says Claude formally proved that 239 entry points across 123 open-source libraries cannot crash

> Working with Theorem, Claude proved in Rocq that OSS-Fuzz tests never hit memory-safety errors on inputs under 64 MB, finding hundreds of bugs on the way.

- Publisher: JARRUS (@jarrus.tech), thejarrus.com
- Story date: Oct. 22, 2026 (2026-10-22)
- Published: 2026-10-27
- Tags: Anthropic, Safety and security, Research
- URL: https://thejarrus.com/en/news/claude-formal-verification/

On October 22, Anthropic's Frontier Red Team published work on using Claude for formal verification at scale. With collaborator Theorem, the team turned existing OSS-Fuzz fuzz tests into formal specifications stating that each test never crashes. Claude then proved them for **239 entry points across 123 libraries**. The proofs show the programs never trigger memory-safety errors or failed assertions for any input under 64 MB. They were written against compiled RISC-V machine code and checked by the Rocq proof checker. Anthropic calls it the first large-scale effort to use AI to apply formal verification to production software.

According to Anthropic, the effort took a few weeks and produced about 180 million lines of Rocq in total, with a typical proof around 600,000 lines. Hundreds of bugs surfaced during the proof attempts, and Claude patched them. Examples include an out-of-bounds write triggered only by rare inputs of about 20 MB and a rediscovery of CVE-2026-56132 in libexpat. On 36 small verification tasks, Opus 5.5 proved half of them using about 40% fewer tokens than Opus 5.

Anthropic stresses that **"formally verified" does not mean "bug-free."** The proofs assume single-threaded RISC-V binaries statically linked with musl libc, while most users run x86 or ARM with dynamically linked glibc. Not every entry point of each library was verified, and a proof can take hundreds of millions of tokens. The company is not releasing proofs that could reveal unpatched bugs.

## Sources

1. [Anthropic: LLMs are making formal software verification feasible at a much larger scale, Oct. 22, 2026](https://www.anthropic.com/research/formal-verification)

Report an error: corrections@thejarrus.com