Anthropic Verifies 123 Open-Source Libraries with Claude

Anthropic said on the 22nd local time that it worked with formal verification company Theorem to use Claude to verify security properties in 123 open-source libraries listed in Google’s OSS-Fuzz. In a few weeks, the team proved across 239 test entry points that all inputs under 64 MB terminate without crashing, and found bugs that existing fuzz tests had missed. Anthropic described the work as the first large-scale AI verification of security properties in production software at the assembly-code level.

Formal verification is a technique that represents a program as a mathematical model and proves that its code always meets specified rules. Because it has traditionally required substantial time and expertise, it has mainly been used for safety-critical software such as avionics systems and operating-system kernels. Implementing the seL4 microkernel took about 2 person-years, while its formal verification took about 20 person-years. Anthropic said advances in AI models’ reasoning abilities have made verification automation and wider use possible.

The experiment used OSS-Fuzz’s existing fuzz tests as its verification benchmark. Fuzz testing repeatedly feeds modified inputs to software to find crashes or errors, but cannot check every execution path. Claude translated tests into mathematical propositions about compiled RISC-V assembly code, then proved normal termination and the absence of memory-safety errors and assertion failures for inputs under 64 MB. The targets were single-threaded static binaries running on RISC-V processors, under specific assumptions including Linux and a fixed memory budget.

The completed proofs total 180 million lines in Rocq format. A typical proof covered a binary with a median of 18,000 RISC-V instructions and included 600,000 lines of proof code. Rocq’s proof checker verifies whether the specifications are met, so people do not need to review the vast code line by line. Reliability still depends on the accuracy of the instruction and Linux process behavior models, the specifications, and the checker.

Claude fixed problems directly during verification and rechecked the modified code, finding hundreds of bugs. In an archive extraction program, it found that a counter underflow with an input of about 20 million bytes and a particular data layout could lead to an out-of-bounds write. In an image decoder, it found an out-of-bounds read involving an input of about 64 million bytes and requiring more than 2 GB of memory. The work also rediscovered a memory access error triggered by calling two handles in a particular order, and CVE-2026-56132 in libexpat, which appears with deeply nested input. It also found a logic error in which a file-loading limit was not always enforced even though no crash occurred.

In separate experiments, Anthropic proved that the Linux kernel’s zlib implementation follows its technical specification and checked whether a Python interpreter written in Rust behaves identically to CPython. It ran more than 1.7 million randomly generated Python programs and found matching behavior in 99.95% of them. In verification of a widely used PDF reader, the team found security bugs at a level typically reported over a year in just one week, as well as logic errors that had remained hidden for more than 10 years in some critical software.

The proofs do not guarantee that all bugs are absent. They cover only inputs under 64 MB and specific execution environments, and make no guarantees about unchecked entry points or behavior on other processors and operating systems. The memory-safety tool ASan also does not catch every memory error. In its own experiments, Anthropic said Opus 5.5 solved half of 36 verification tasks using about 40% fewer tokens than Opus 5; when multiple AI agents shared proofs, token use fell 17% compared with individual work. Anthropic released some proofs and verification models for developers to reuse or apply to their own code. Theorem is also helping other open-source projects use the same process.

Anthropic said on the 22nd local time that it worked with formal verification company Theorem to use Claude to verify security properties in 123 open-source libraries listed in Google’s OSS-Fuzz. In a few weeks, the team proved across 239 test entry points that all inputs under 64 MB terminate without crashing, and found bugs that existing fuzz tests had missed. Anthropic described the work as the first large-scale AI verification of security properties in production software at the assembly-code level.

Formal verification is a technique that represents a program as a mathematical model and proves that its code always meets specified rules. Because it has traditionally required substantial time and expertise, it has mainly been used for safety-critical software such as avionics systems and operating-system kernels. Implementing the seL4 microkernel took about 2 person-years, while its formal verification took about 20 person-years. Anthropic said advances in AI models’ reasoning abilities have made verification automation and wider use possible.

The experiment used OSS-Fuzz’s existing fuzz tests as its verification benchmark. Fuzz testing repeatedly feeds modified inputs to software to find crashes or errors, but cannot check every execution path. Claude translated tests into mathematical propositions about compiled RISC-V assembly code, then proved normal termination and the absence of memory-safety errors and assertion failures for inputs under 64 MB. The targets were single-threaded static binaries running on RISC-V processors, under specific assumptions including Linux and a fixed memory budget.

The completed proofs total 180 million lines in Rocq format. A typical proof covered a binary with a median of 18,000 RISC-V instructions and included 600,000 lines of proof code. Rocq’s proof checker verifies whether the specifications are met, so people do not need to review the vast code line by line. Reliability still depends on the accuracy of the instruction and Linux process behavior models, the specifications, and the checker.

Claude fixed problems directly during verification and rechecked the modified code, finding hundreds of bugs. In an archive extraction program, it found that a counter underflow with an input of about 20 million bytes and a particular data layout could lead to an out-of-bounds write. In an image decoder, it found an out-of-bounds read involving an input of about 64 million bytes and requiring more than 2 GB of memory. The work also rediscovered a memory access error triggered by calling two handles in a particular order, and CVE-2026-56132 in libexpat, which appears with deeply nested input. It also found a logic error in which a file-loading limit was not always enforced even though no crash occurred.

In separate experiments, Anthropic proved that the Linux kernel’s zlib implementation follows its technical specification and checked whether a Python interpreter written in Rust behaves identically to CPython. It ran more than 1.7 million randomly generated Python programs and found matching behavior in 99.95% of them. In verification of a widely used PDF reader, the team found security bugs at a level typically reported over a year in just one week, as well as logic errors that had remained hidden for more than 10 years in some critical software.

The proofs do not guarantee that all bugs are absent. They cover only inputs under 64 MB and specific execution environments, and make no guarantees about unchecked entry points or behavior on other processors and operating systems. The memory-safety tool ASan also does not catch every memory error. In its own experiments, Anthropic said Opus 5.5 solved half of 36 verification tasks using about 40% fewer tokens than Opus 5; when multiple AI agents shared proofs, token use fell 17% compared with individual work. Anthropic released some proofs and verification models for developers to reuse or apply to their own code. Theorem is also helping other open-source projects use the same process.