Anthropic Says Claude Generated Assembly-Level Formal Proofs for 123 Open-Source Libraries

Anthropic has partnered with formal verification company Theorem to convert existing fuzz tests in open-source projects into mathematical specifications, which Claude then writes proofs for and submits to the Rocq proof checker for verification. Anthropic reported that the team completed proofs for 123 open-source libraries and 239 test entry points within weeks, covering approximately 180 million lines of proof code. The core conclusion is that, for inputs smaller than 64 MB, under defined Linux response and memory layout conditions, the test entry points—after being patched and compiled into specific RISC-V programs—do not crash due to memory safety errors or assertion failures. While writing proofs, Claude also identified and patched issues previously missed by testing, including out-of-bounds reads and writes triggered only by rare inputs. Compared with fuzz testing, which relies on repeated sampling, formal proofs provide exhaustive coverage of all inputs within the defined scope; however, the validity of the conclusions depends on the accuracy of the specifications, machine model, and proof checker. Current proofs primarily target specific runtime conditions such as single-threaded execution and static linking, and do not cover all code in each library. Anthropic has published some proofs publicly for external review and reuse. This study demonstrates the potential for AI to reduce the effort required for formal verification, but it does not justify claiming that the 123 libraries are "vulnerability-free."