Anthropic says Claude proved security properties in 123 open-source libraries

Anthropic said its Claude models were able to produce formal proofs for security properties in compiled code across 123 open-source libraries, a result the company described as a step toward making formal software verification practical at much larger scale. In the research post published on Oct. 22, 2026, Anthropic said the work also surfaced bugs that had gone unnoticed for years.

Evidence and context

According to Anthropic, Claude proved that 239 entry points across those 123 libraries would not crash on any input below 64 MB under the project’s modeled conditions. The company said the proofs were applied at the assembly-code level on RISC-V binaries and used Theorem’s formal semantics for RISC-V and Linux process behavior. Anthropic said the effort covered real-world open-source software, including libraries from Google’s OSS-Fuzz initiative, and that it represents, to its knowledge, 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 and that Claude also patched bugs it encountered during the process. Among the examples listed were an out-of-bounds write triggered by a rare 20 MB input layout, an out-of-bounds read in an image decoder requiring a 64 MB input and more than 2 GB of memory, a crash tied to a particular call sequence across two file handles, and a rediscovery of CVE-2026-56132 in libexpat. Anthropic also said the effort uncovered logic bugs that did not crash the software, including one case in which a file-access restriction feature was not always enforced.

The company said the proofs are conditional and do not imply the software is bug-free. Its own limitations section says the guarantees depend on modeled assumptions, including single-threaded static binaries with a fixed memory budget running on RISC-V Linux, and that the work does not cover all entry points or all ways software may be used in production. Anthropic said the remaining uncertainty is concentrated in the trusted components: the RISC-V and Linux semantics, the theorem statements, and the Rocq proof checker.

Why it matters

Anthropic framed the work as evidence that LLMs can reduce the cost of formal verification, which has historically required highly specialized effort and has usually been confined to mission-critical systems. The post says larger models needed fewer tokens for some verification tasks, while shared proof components reduced duplication across related projects. The company also said it plans to publish a subset of the proofs and that Theorem will offer the same pipeline for other open-source projects.

The research is consistent with wider industry work showing that formal verification can complement testing rather than replace it. But as Anthropic itself notes, the value of a proof still depends on whether the specification and machine model match reality, and many deployment assumptions remain outside the scope of the verified claims.