This is potentially very good news for cybersecurity. For example, today things like video codecs and font renderers are a common source of vulnerabilities. It may be practical before too long for browser vendors, at least, to use fuzz tests and AI to prove that their codecs have no security bugs, and then attackers would have to look for things like OS bugs or hardware glitches.
If that happens, it will be at least as important as Rust is for memory safety.
Eventually, after AI has been optimized for this and there are suitable software packages available that implement it, ordinary software engineers will be able to run AI on their fuzz tests overnight to prove that a new release is free of many classes of security bugs.
And if you don't do that, attackers probably will, because it will find any security bugs that exist.
I was rather skeptical about how important formal verification would be for software, but if it can be almost fully automated, it will become essential. You don't need to know a lot of math to write fuzz tests.
For this project, we started with fuzz tests. In these tests, developers write an entry point2 into their code that takes inputs, such that any input that causes a crash is a bug the authors care about. Then the fuzzer, a testing engine, generates enormous numbers of semirandom and mutated inputs at the entry point to try to find a bug (visualized in Figure 1). The longer a fuzzer runs, the more bugs it can find. But this is inherently a brute-force process, with no guarantee of exercising every possible code path, regardless of how many inputs you try.
[...]
To find all the bugs that would’ve been surfaced by a fuzz test, we turned the fuzz test into a spec defined over the compiled RISC-V instructions. The spec says that the fuzz test won’t crash for any input less than 64 MB.3 If Claude can prove this spec, the fuzz test on RISC-V becomes superfluous: fuzzing that entry point will never find any bugs.
We did this for hundreds of projects in Google’s OSS-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects. OSS-Fuzz contains thousands of developer-authored entry points that look for broken code properties by crashing (for example, on a failed assertion). OSS-Fuzz automatically instruments C and C++ programs with AddressSanitizer4 (ASan), causing them to crash whenever memory is accessed improperly (which is a leading cause of software vulnerabilities). Broad-spectrum specifications like memory safety apply to almost all software.
[...]
Over the span of a few weeks, Claude successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries. These proofs operate on the compiled RISC-V instructions (i.e., executable binaries), and they comprise about 180 million lines of Rocq, with a typical proof running to about 600,000 lines to provide security guarantees on binaries with a median length of 18,000 RISC-V instructions. These proofs are built by translating the RISC-V assembly code to a mathematical model using Theorem’s RISC-V instruction and Linux process semantics. This means these proofs currently assume that the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux OS. Expanding the scope of these proofs is well within reach, as it would involve standardizing semantics for more assembly architectures and other operating system processes. See an expert’s take on the proofs Claude wrote.
[...]
This doesn’t mean these libraries contain no bugs. Instead, it means that any remaining bugs either are to be found within the artifacts listed above or are outside the scope of Claude’s proof. Hardening those still-possibly-buggy trusted components (Rocq, RISC-V, and Linux semantics) is not insignificant, but it’s a far more tractable task than debugging every line of code the scaled-out proofs cover—especially as this approach can secure an arbitrary number of projects without increasing the size of the trusted components.
[...]
Many of the bugs we found are ones that a fuzzer would be unlikely to ever find. Fuzzers mutate small inputs, typically capped at 1 MB, and typically rely on code coverage to guide them toward bugs. While proving an entry point in one library, Claude found a counter underflow in its copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB that had one rare, specific layout. Other bugs include an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory, an out-of-bounds read in another library that needed a particular sequence of calls across two handles to the same file, and a rediscovery of CVE-2026-56132 in libexpat, which needed deeply nested input. Claude also found logic bugs that never crash at all. While proving that one library was memory-safe, for example, it noticed that a feature for restricting which files an application can load isn’t always enforced.
[...]
Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.
This can also occur even when the properties are not directly specified by the developer. For example, in order for Claude to complete its OSS-Fuzz proof for cpp-httplib, it was necessary to rule out the possibility of a stack overflow due to too much recursion in the std::set destructor. This recursion depth is bounded by the maximum depth of a tree, so Claude had to prove (on machine code!) that libc++’s red-black tree rebalancing algorithm is correctly optimized to keep the tree’s depth logarithmically bounded.
[...]
In another experiment, we asked Claude to develop an interpreter for a large subset of Python in Rust, and to prove (using Verus, a verification tool for Rust) that it adheres to the CPython semantics outlined in an academic paper. We then measured the adherence to CPython’s behavior empirically, running over 1.7 million randomly generated Python programs, finding identical behavior with CPython in 99.95% of tests, with remaining test differences as unsurprising known corner cases.
We also found issues in several widely used and critical applications via formal verification attempts of simple security properties. In one of them, we discovered a previously unknown logic bug that had been latent for more than a decade. During an effort to verify a widely used PDF reader, we found as many security bugs in one week as are typically reported in a year.
[...]
This reusability of proofs is how Mathlib, a shared library of formal mathematics in Lean, grew to nearly 300,000 theorems submitted by over 700 contributors: each new proof builds on the existing body of work. We accumulated a similar body of proofs in the course of our OSS-Fuzz effort, some of which we’re including in our release (we are not releasing proofs that may reveal an unpatched bug in the open-source software).
I'm glad this is working out. The HN thread about this noted that some folks are trying it out on their own codebases, and it's been useful for e.g. proving that CUDA code is semantically identical to some other GPGPU platform's code, or even doing things as crazy as porting PostgreSQL to Rust (as a side project).
I think I'd noted it on Tildes before, so apologies for sounding like a broken record, but I very strongly believe it's possible to define confidentiality, integrity, and availability constraints for practically all software domains. So I've held out hope for a while that auto-formalization will be the solution to the barrage of holes poked in foundational software. This is a nice stepping stone in that direction, although it needs to hit the next round of model pretraining datasets before we really start seeing it take off I imagine.
[OP] skybrian | 17 hours ago
This is potentially very good news for cybersecurity. For example, today things like video codecs and font renderers are a common source of vulnerabilities. It may be practical before too long for browser vendors, at least, to use fuzz tests and AI to prove that their codecs have no security bugs, and then attackers would have to look for things like OS bugs or hardware glitches.
If that happens, it will be at least as important as Rust is for memory safety.
Eventually, after AI has been optimized for this and there are suitable software packages available that implement it, ordinary software engineers will be able to run AI on their fuzz tests overnight to prove that a new release is free of many classes of security bugs.
And if you don't do that, attackers probably will, because it will find any security bugs that exist.
I was rather skeptical about how important formal verification would be for software, but if it can be almost fully automated, it will become essential. You don't need to know a lot of math to write fuzz tests.
[OP] skybrian | a day ago
From the article:
[...]
[...]
[...]
[...]
[...]
[...]
[...]
kacey | 3 hours ago
I'm glad this is working out. The HN thread about this noted that some folks are trying it out on their own codebases, and it's been useful for e.g. proving that CUDA code is semantically identical to some other GPGPU platform's code, or even doing things as crazy as porting PostgreSQL to Rust (as a side project).
I think I'd noted it on Tildes before, so apologies for sounding like a broken record, but I very strongly believe it's possible to define confidentiality, integrity, and availability constraints for practically all software domains. So I've held out hope for a while that auto-formalization will be the solution to the barrage of holes poked in foundational software. This is a nice stepping stone in that direction, although it needs to hit the next round of model pretraining datasets before we really start seeing it take off I imagine.