Anthropic company presented results experiments on the use of AI models for formal verificationof reliability and safety of existing projects. During the experiment, using AI models for 123 open-source libraries tested in the OSS Fuzz infrastructure, mathematical proofs of the absence of errors when working with memory were generated.
Testing was carried out at the level of compiled assembly code for the RISC-V architecture. The total volume of generated evidence was about 180 million lines of code for the Rocq Prover verification system (about 600 thousand lines per binary file with 18 thousand RISC-V instructions). The proofs were generated by automatically converting existing fuzzing tests into formal specifications, after which the Claude AI model proved that the program did not crash for any input data up to 64 MB.
In the process of building the proofs, the AI model was able to identify and prepare fixes for hundreds of errors that had not previously been noticed during fuzzing testing. Among other things, vulnerabilities were identified that lead to buffer overflows when processing certain input data (for example, CVE-2026-56132 in libexpat), as well as logical errors. In addition, the AI model was used to prove compliance of the implementation of the zlib algorithm in the Linux kernel with the specification RFC 1950.
An interpreter was also generated in the Rust language for a subset of the Python language, for which, using the Verus has prepared a formal proof of compliance with CPython semantics. To compare behavior with CPython, more than 1.7 million randomly generated Python programs were executed. In 99.95% of cases, the results of executing these programs in the new implementation and in CPython coincided, and the identified discrepancies turned out to be known edge cases.
The formal verification ensures compliance with the specification, but does not completely exclude the occurrence of security problems, since the risks caused by problems with multithreading, dynamic linking and anomalous behavior of real equipment do not remain formalized. The key advantage of the proposed approach is working directly with binary files, which eliminates the need to rewrite existing code in formally verifiable languages.