Anthropic says Claude produced formal proofs that 123 open-source libraries' fuzz tests cannot crash
The company reports its model checked compiled code at the assembly level and found hundreds of bugs along the way, including some that years of testing had missed.
Anthropic says its Claude model has written formal proofs of security properties for compiled code in 123 open-source software libraries. This account rests on a single source: a research post published by Anthropic about its own model.
According to Anthropic, the work was done with a company called Theorem. Over a few weeks, Claude proved that 239 entry points across 123 libraries in Google's OSS-Fuzz testing program will not crash on any input up to 64 MB. The proofs cover the compiled RISC-V assembly instructions, not just the source code. Anthropic said they total about 180 million lines in the Rocq proof language. A typical proof runs to about 600,000 lines, covering programs with a median length of 18,000 instructions.
Anthropic described this as, to its knowledge, the first large-scale effort to use AI to formally verify production software at the assembly level.
The company says this matters because formal verification has usually been too expensive for most projects. As one example, Anthropic said that building the seL4 operating system kernel took two person-years, while formally verifying it took 20. It pointed to the Linux kernel, which it said recently had more than 1,000 vulnerabilities disclosed, as a sign that even heavily tested software has flaws.
“Most software is riddled with bugs, which AI can now easily find and exploit.”Anthropic research post
While writing the proofs, Claude found and patched hundreds of bugs, Anthropic said. These included an out-of-bounds write in a decompressor that appeared only with inputs of around 20 MB in one rare layout, and an out-of-bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory. Anthropic said fuzzers, which usually test small inputs, would be unlikely to find bugs like these. It also said Claude rediscovered a known vulnerability in the libexpat library.
Much is still unclear. The results come from Anthropic itself and have not been independently checked. The company says it is publishing a subset of the proofs and the supporting models of RISC-V and Linux behavior, and it has invited others to verify them.
The guarantees are also narrow. Anthropic said the proofs assume a single-threaded static program with a fixed memory budget running on a RISC-V processor under Linux. In its words, "This doesn’t mean these libraries contain no bugs." Any remaining bugs fall outside the proofs' scope or sit in the tools the proofs depend on.
The post does not say whether the library maintainers have accepted Claude's patches. It also does not say how the approach would work on other processor types or on multi-threaded software, though Anthropic says expanding the scope is "well within reach."
Theorem is offering to run the same process for other open-source projects, Anthropic said.
