Key takeaways:
- AI is expanding verification: Claude generated formal proofs across 123 open-source libraries, demonstrating the potential to scale software security checks.
- Hidden bugs are easier to identify: AI-assisted verification uncovered hundreds of defects that conventional testing could miss.
- Security guarantees remain conditional: Wider adoption depends on reducing verification costs, improving system models, and proving a broader range of software behaviours.
1. AI makes formal software verification more accessible
Large language models (LLMs) are making formal software verification more practical, potentially transforming how developers identify and prevent security vulnerabilities. In research published on October 22, 2026, Anthropic’s Frontier Red Team, working with software verification company Theorem, demonstrated how its Claude model could generate mathematical proofs for selected security properties across 123 open-source software libraries.
Traditional software testing relies on running programs against different inputs to identify errors. However, even extensive testing cannot guarantee that every possible bug has been detected. Formal verification addresses this limitation by using mathematical proofs to establish whether software meets specific requirements under defined conditions.
Historically, this process has required specialised expertise and substantial time. For example, formally verifying the seL4 operating system kernel took considerably longer than implementing it, limiting the technique’s use largely to safety-critical applications.
The research team used Google’s OSS-Fuzz programme, which continuously tests open-source software for vulnerabilities, to demonstrate how AI formal verification could reduce this workload. The team converted existing fuzz tests into formal specifications and asked Claude to prove that the corresponding compiled programs would not crash under specified conditions.
The experiment covered 239 test entry points across 123 open-source libraries. Claude generated approximately 180 million lines of Rocq proof code, which were checked using the Rocq proof assistant.
The findings suggest that AI could help developers incorporate formal verification into everyday software development, extending its benefits beyond specialised, high-security systems.
2. AI uncovers bugs missed by conventional testing
The experiment delivered another significant result: Claude discovered and helped fix hundreds of bugs while attempting to prove that the software met its specifications. Some defects had remained undetected despite extensive testing because they required unusual inputs, specific execution sequences, or substantial memory resources to trigger.
One decompression-related bug involved a counter underflow that could cause an out-of-bounds write when processing an approximately 20 MB input with a particular structure. Another vulnerability involved an image decoder that required a 64 MB input and more than 2 GB of memory to expose an out-of-bounds read.
The research also identified a previously reported vulnerability in the libexpat library and uncovered a logic error affecting restrictions on which files an application could load.
These findings highlight the difference between fuzzing and formal verification. Fuzzing generates large numbers of inputs to identify failures, but it cannot exhaustively test every possible scenario. Formal verification attempts to prove that a particular property holds across the entire input range defined by its specification.
The researchers also explored other applications of AI formal verification. These included checking whether the Linux kernel’s zlib implementation followed its formal specification and developing a Rust-based interpreter that matched CPython’s behaviour. The interpreter produced identical results in 99.95% of more than 1.7 million randomly generated Python program tests.
However, the researchers cautioned that proving selected properties does not establish that an entire application is completely free of bugs. The results depend on the accuracy of the specifications and the assumptions used to model the underlying hardware and operating system.
3. Reusable proofs could reduce costs and expand adoption
Despite the promising results, the cost of generating formal proofs remains a major challenge. Such tasks can consume enormous amounts of computing resources, making efficiency essential for wider adoption.
The research team found that newer models could complete verification tasks using fewer tokens. In an experiment involving 36 verification tasks, AI agents that shared and reused one another’s proofs required 17% fewer tokens than agents working independently.
Reusable proofs could make AI formal verification more efficient because many software projects depend on common libraries and components. Verifying these dependencies once and adapting existing proofs could reduce duplicated work and strengthen security across multiple applications.
Nevertheless, the current approach has limitations. The proofs rely on specific conditions, including single-threaded execution, static binaries, a fixed memory budget, and a RISC-V processor running Linux. They also cover selected test entry points and inputs smaller than 64 MB, rather than every possible behaviour of an entire library.
The research points towards a future in which AI formal verification becomes a standard software development practice alongside conventional testing and static analysis. Achieving that goal will require more efficient models, broader system coverage, and accurate specifications that reflect real-world operating conditions.
