Anthropic has released the results of experiments utilizing AI models for the formal verification of the reliability and safety of existing projects. During the experiment, AI models were used to generate mathematical proofs of the absence of memory errors for 123 open libraries tested in the OSS Fuzz infrastructure.
The verification was conducted at the compiled assembly code level for the RISC-V architecture. The total volume of generated proofs amounted to approximately 180 million lines of code for the verification system Rocq Prover (around 600,000 lines for a binary file with 18,000 RISC-V instructions). The proofs were formed by automatically converting existing fuzzing tests into formal specifications, after which the AI model Claude demonstrated that no crashes occur in the program with any input data up to 64 MB.
In the process of constructing the proofs, the AI model was able to identify and prepare patches for hundreds of bugs previously unnoticed during fuzzing testing. Among other things, vulnerabilities leading to buffer overflows when processing certain input data were discovered (for instance, CVE-2026-56132 in libexpat), as well as logical errors. In addition, the AI model was used to prove compliance of the zlib algorithm implementation in the Linux kernel with the RFC 1950 specification.
An interpreter for a subset of the Python language was also generated in Rust, for which a formal proof of conformance to the CPython semantics was prepared using the Verus toolkit. To compare the behavior with CPython, over 1.7 million randomly generated Python programs were executed. In 99.95% of cases, the execution results of these programs in the new implementation and in CPython matched, and the identified discrepancies turned out to be known edge cases.
Formal verification ensures compliance with specifications, but does not completely eliminate the potential for security issues, as risks associated with multithreading, dynamic linking, and abnormal behavior of real hardware remain unformulated. A key advantage of the proposed approach is the ability to work directly with binary files, thus avoiding the need to rewrite existing code in formally verifiable languages.
Source: opennet.ru
