LLMs generate formal proofs to secure open-source software

The limits of traditional testing

Most modern software is filled with bugs that hackers can exploit. While developers use standard defenses, these are often insufficient against sophisticated attacks. To truly secure code, engineers need a way to prove that a program is free of specific vulnerabilities.

This is where formal software verification comes in. In this process, developers translate their code into a mathematical model and then try to prove it follows a set of security rules. If the proof fails, it indicates a bug exists. However, this has historically been impractical because the proofs are often many times larger than the original code and require highly specialized expertise.

For example, it took 20 person-years to formally verify the seL4 operating system kernel. Because of this high cost, formal verification was usually reserved for mission-critical systems, like the avionics code used in Airbus aircraft. Anthropic is now using LLMs to change that dynamic by making the process feasible for a much wider range of projects.

Turning tests into proofs

To prove software is correct, you first have to define what 'correct' means. For many complex programs, like web browsers or text editors, writing a complete specification is a massive hurdle. To solve this, Anthropic and their collaborator Theorem took a different approach: they converted existing compilable test suites into specifications.

They used a method where they encoded the rule that a specific test suite must always pass. They specifically looked at fuzz tests, which are engines that generate millions of random inputs to try and crash a program. By turning these into formal specs, they created a goal for the AI: prove that the program will never crash for any input smaller than 64 MB.

Using Claude, the team successfully patched bugs and then proved these specs for 239 entry points across 123 different libraries. The AI churned through millions of lines of code to reach these goals. Because the Rocq proof checker ensures the spec is satisfied, developers only need to trust the core models, the theorem statements, and the checker itself, rather than manually reviewing every line of the generated proof.

Discovering hidden vulnerabilities

The process of attempting to prove these specifications yielded significant results. While the goal was to prove the absence of crashes, the effort revealed hundreds of bugs that were previously unknown. Many of these were bugs that traditional fuzzers would likely never find because they required very specific, rare inputs or complex sequences of calls.

For instance, Claude found a counter underflow in a decompressor that only triggered on inputs around 20 MB with a specific layout. It also found an out-of-bounds read in an image decoder that required a 64 MB input and over 2 GB of memory. In some cases, the AI even discovered logic bugs where features intended to restrict file loading were not properly enforced.

Beyond just finding crashes, the AI had to prove complex properties to complete its tasks. To verify a specific library, Claude had to prove on the machine code level that a standard library's tree rebalancing algorithm was correctly optimized to keep the tree's depth bounded. This demonstrates that LLMs can now handle the heavy lifting required for deep software analysis.

A roadmap for secure code

As models become more intelligent, the cost of writing these proofs continues to fall. Anthropic expects formal verification to become an essential part of secure software development as methods for achieving security guarantees become more standardized. The ability to reuse or modify proofs across different codebases will help reduce the effort required for new projects.

The team is already publishing a subset of these proofs and the RISC-V and OS semantics so that others can verify and reuse them. They are also offering to run this pipeline for other open-source projects. This work provides a roadmap for moving toward a world where software security is not just tested, but mathematically guaranteed.

Expanding the scope

While the current proofs assume the program runs as a single-threaded static binary on a RISC-V CPU using Linux, expanding this scope is considered well within reach. This would involve standardizing the mathematical semantics for more assembly architectures and different operating system processes.

The team has also explored other formal verification methods to accelerate different tasks. These include assessing the security of the zlib compression algorithm and proving that a Python interpreter written in Rust is behaviorally equivalent to its original version. These experiments suggest that LLMs can be used to root out long-standing bugs in many types of critical software.