Anthropic said its Claude AI models produced formal proofs for security properties in compiled code across 123 open-source libraries. The company shared the results in a research post published on Oct. 22, 2026.
Anthropic said the work also found bugs that had gone unnoticed for years. It described the project as a step toward making formal software verification practical at a much larger scale.
What Claude Proved
According to Anthropic, Claude proved that 239 entry points across the 123 libraries would not crash on any input smaller than 64 MB. This result applies under the conditions modeled by the project.
The proofs were applied at the assembly-code level on RISC-V binaries. They relied on Theorem’s formal semantics for RISC-V and Linux process behavior.
The effort covered real-world open-source software, including libraries from Google’s OSS-Fuzz initiative. Anthropic said that, to its knowledge, this is the first large-scale use of AI to apply formal verification to production software at the assembly-code level.
The company said the proofs were generated over several weeks. Claude also patched bugs it found along the way.
Bugs Found and Limits of the Proofs
Anthropic listed several examples of bugs uncovered during the work. One was an out-of-bounds write triggered by a rare 20 MB input layout.
Another was an out-of-bounds read in an image decoder. That bug required a 64 MB input and more than 2 GB of memory to trigger.
Claude also found a crash tied to a specific call sequence across two file handles. It rediscovered CVE-2026-56132 in the libexpat library as well.
Some bugs did not cause crashes. Anthropic said the work found logic bugs, including one case where a file-access restriction feature was not always enforced.
Anthropic said the proofs are conditional and do not mean the software is free of bugs. The guarantees depend on modeled assumptions.
Those assumptions include single-threaded static binaries with a fixed memory budget running on RISC-V Linux. The work also does not cover every entry point or every way the software may be used in production.
The company said the remaining uncertainty sits in trusted components. These include the RISC-V and Linux semantics, the theorem statements, and the Rocq proof checker.
Anthropic said the work shows large language models can lower the cost of formal verification. That process has usually required highly specialized effort and has mostly been limited to mission-critical systems.
The post said larger models needed fewer tokens for some verification tasks. Shared proof components also reduced repeated work across related projects.
Anthropic said it plans to publish a subset of the proofs. Theorem will also offer the same pipeline to other open-source projects.
