Anthropic says Claude formally verified 123 open-source libraries

Anthropic announced on October 22 that Claude was used, in collaboration with formal-proof specialist Theorem, to formally verify security properties of 123 open-source libraries registered in Google's OSS-Fuzz project.

According to aitimes.com, Claude completed proofs for 239 test entry points across those libraries, showing the tests terminate without crashes for all inputs under 64MB, including no memory-safety errors or assertion failures. The generated proofs totaled 180 million lines in the Rocq proof-assistant format, with a median proof covering a binary of about 18,000 RISC-V instructions.

The company said Claude found hundreds of bugs while working, fixed the code and then re-proved the fixes. Examples include a counter underflow in a decompressor and an out-of-bounds read in an image decoder. The work also rediscovered CVE-2026-56132 in the libexpat XML parser library.

Anthropic described the result as the first large-scale AI verification of security properties of production software at the assembly code level. It released some of the proofs and the model used for the verification, and Theorem is offering support to apply the same process to other open-source projects.

In a separate experiment, Opus 5.5 solved half of 36 verification tasks using about 40% fewer tokens than Opus 5, and agent collaboration reduced token use by 17%.

Why it was mostly limited before

Formal verification has previously been applied mainly to safety-critical software such as avionics systems and OS kernels, because it demanded large amounts of time and expertise. Verifying the seL4 microkernel took about 2 person-years to implement but about 20 person-years to formally verify.