Anthropic says Claude, working with formal-methods firm Theorem, turned OSS-Fuzz fuzz targets into formal specs and proved them in the Rocq proof assistant. The result covers 239 entry points across 123 libraries: for every input under 64 MB, the compiled binaries never fault, abort or hit unmodeled behavior.

• Scope: the proofs are over compiled RISC-V binaries, single-threaded and static, with a fixed memory budget, under Theorem's Linux process semantics, which Theorem calls best-effort and incomplete. They show the ASan-instrumented and normal binaries behave the same. They don't cover other CPUs, threads or properties beyond crashes and memory safety.
• Size: about 180 million lines of Rocq, typically about 600,000 per proof, for binaries with a median of 18,000 instructions, done over a few weeks.
• Bugs found along the way, which Claude patched before proving: a counter underflow in a bundled decompressor causing an out-of-bounds write only on ~20 MB inputs with one rare layout, an image-decoder out-of-bounds read needing a 64 MB input, and a rediscovery of libexpat CVE-2026-56132.

A subset of proofs and the semantics are public, and Theorem is offering to run the pipeline for other open-source projects (OSS Verify). Why it matters: AI-driven bug finding is fueling this month's flood of critical CVEs, and this is the defensive side of the same capability.