Anthropic says Claude proved 239 entry points in 123 open-source libraries free of crashes, and found hundreds of bugs on the way

Anthropic's Frontier Red Team, working with its collaborator Theorem, published a paper on 22 October titled “LLMs are making formal software verification feasible at a much larger scale”. Claude was asked to prove useful security properties across 123 open-source libraries.

The paper says Claude, sometimes after patching bugs it found, proved that there are no crashes on any input, up to 64 MB, for 239 entry points across the 123 libraries, which come from Google's OSS-Fuzz project. The proofs come to about 180 million lines in the Rocq proof checker. The paper says the process of attempting the proofs “discovered hundreds of bugs.”

The paper sets its own limits. The proofs cover the code after Claude's patches, and assume single-threaded static programs built with musl libc, running on Linux on RISC-V. Most real deployments, on x86 or ARM with glibc, are not covered. In a separate exercise on zlib and half a dozen other widely used libraries, the paper says, some minor, unexploitable bugs were found and are being filed upstream. Anthropic is not releasing proofs that may reveal an unpatched bug.

• Claimed Claude proved there are no crashes on inputs up to 64 MB for 239 entry points across 123 open-source libraries. Anthropic, “LLMs are making formal software verification feasible at a much larger scale”
• Claimed The proofs total about 180 million lines of Rocq, and attempting them discovered hundreds of bugs. Anthropic
• Confirmed The paper says the proofs cover the patched code under narrow assumptions (musl libc, Linux, RISC-V), and that Anthropic is not releasing proofs that may reveal an unpatched bug. Anthropic