Claude proves security properties of 123 open source libraries

For decades, formal verification has been the gold standard of software security that almost nobody could afford. You write a mathematical proof that a program can never do something bad, a machine checks the proof, and then you know, instead of hoping. The catch has always been the price. On 22 October 2026, Anthropic's Frontier Red Team and the verification startup Theorem published results suggesting that price is collapsing: Claude wrote machine checked proofs of security properties for compiled code in 123 open source libraries, and found bugs along the way that years of testing had not.

The work is described in a long post on the Anthropic research blog, also featured on the Theorem blog. Theorem supplied the formal models of the processor and of Linux that the proofs rest on. According to Anthropic, this is the first large scale effort to use AI to apply formal verification to production software at the assembly code level.

The short version

• Claude proved that 239 fuzz test entry points across 123 libraries from Google's OSS-Fuzz program never crash on any input smaller than 64 MB.
• The proofs are about the compiled RISC-V machine code, not the source. They total about 180 million lines of Rocq, with a typical proof around 600,000 lines for a binary with a median length of 18,000 instructions.
• Every proof is checked by the Rocq proof kernel, so humans do not need to read them.
• Trying to write the proofs surfaced hundreds of bugs, including some that would need a 20 MB or 64 MB input to trigger, well beyond what fuzzers usually try.
• A subset of the proofs and the RISC-V and Linux semantics are public. Theorem now offers the same pipeline free to qualifying open source projects and ships a Claude skill to help maintainers enroll.
• The guarantee is narrow and the authors say so: "formally verified" does not mean "bug free".

Why formal verification was out of reach

Testing shows that a program works for the inputs you tried. A proof shows that it works for all of them. The difference matters more every month, because the same AI models that can write code can also scan it for weaknesses and chain small bugs into working exploits. Anthropic points to the Linux kernel, one of the most tested pieces of software in the world, which recently had more than 1,000 vulnerabilities disclosed.

The problem is effort. Proofs are often many times larger than the code they describe, and writing them takes a rare skill set. The classic example is seL4, a verified operating system kernel: building it took about two person years, verifying it took about 20. That is why formal methods have mostly stayed in places like aircraft control software, where failure is not an option and budgets reflect that.

Anthropic's argument is that this ratio has changed. Grinding through millions of lines toward a precise, checkable goal is close to an ideal task for a language model. The model can be wrong as often as it likes along the way, because the proof checker throws out anything that does not hold.

How tests become proofs

The hardest part of verification is often not the proof but the question of what "correct" means. For a PNG decoder there is a standard to follow. For a text editor or a browser there is no neat definition.

The team side stepped that problem with a clever choice. Many open source projects already have fuzz tests: small entry points that take arbitrary bytes, feed them into the library and crash if something goes wrong. Google's OSS-Fuzz program runs thousands of these continuously and compiles C and C++ projects with AddressSanitizer, which turns memory errors such as buffer overflows into immediate crashes. A fuzzer then throws huge numbers of random and mutated inputs at each entry point, hoping to hit a crash. It can run forever and still never prove that no crash exists.

So the team turned each fuzz test into a specification: this entry point, compiled to RISC-V, never crashes for any input smaller than 64 MB. If Claude can prove that statement, fuzzing that entry point on RISC-V can never find another bug, no matter how long it runs.

The mechanics, as Anthropic describes them:

• The library and its fuzz test are compiled into a static RISC-V executable.
• Theorem's formal semantics of RISC-V instructions and of a Linux process turn that binary plus the no crash rule into a precise mathematical statement.
• Claude writes a proof of that statement in Rocq, the proof assistant formerly known as Coq.
• The Rocq kernel checks the proof. Either it is valid or it is rejected.

The proved property is stronger than it first sounds. Claude showed that the programs always exit normally, without memory safety errors or failed assertions, for every input under 64 MB and for every modeled response from the operating system and every memory layout. And because many fuzz tests crash on purpose when a deeper property breaks, a no crash proof can carry real meaning. The LZO compression fuzz test, for example, checks that compressing and then decompressing gives back the original data. Proving that this test never crashes is the same as proving the round trip always works.

Sometimes the proof forced Claude to establish facts nobody had asked for. To finish the proof for cpp-httplib, it had to rule out a stack overflow from deep recursion in a C++ set destructor. That meant proving, on machine code, that the red black tree code in libc++ really keeps the tree depth logarithmically bounded.

The numbers

Over a few weeks, Claude patched the bugs it found and then proved the no crash property for 239 entry points across 123 libraries. The proofs add up to about 180 million lines of Rocq. A typical proof runs to about 600,000 lines and covers a binary with a median size of 18,000 RISC-V instructions.

Nobody is expected to read those 180 million lines. That is the point of a proof checker. What a developer has to trust is short: the formal models of RISC-V and of Linux processes, the exact theorem statements, and the Rocq checker itself. If those are right, the proof is right. Hardening a small trusted core is a much more tractable job than auditing every library the proofs cover, and that core does not grow as more projects are verified.

Bugs that fuzzing would not find

You cannot prove something false. Every time a proof attempt hit a real bug, Claude had to stop and deal with it. To keep the process running without a human in the loop, the team let Claude patch the code, regenerate the specification from the patched version and prove that instead. Across hundreds of entry points, that surfaced hundreds of bugs.

Many of them are the kind a fuzzer is unlikely to ever reach. Fuzzers usually mutate small inputs, often capped at around 1 MB, and follow code coverage. Examples from the post:

• A counter underflow in a library's copy of a decompressor that led to an out of bounds write, but only for inputs around 20 MB with one rare layout.
• An out of bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory.
• An out of bounds read that required a particular sequence of calls across two handles to the same file.
• A rediscovery of CVE-2026-56132 in libexpat, which needed deeply nested input.
• A logic bug that never crashes at all: a feature meant to restrict which files an application can load was not always enforced.

Letting the model patch code it is trying to prove opens an obvious loophole. Claude could make any theorem provable by rewriting the program into one that trivially never crashes. Anthropic says it penalized every patch, gave extra credit for proving exactly which inputs a patch changed and how few, and logged and audited the patches for this kind of reward hacking. That is a sensible safeguard, and also a reminder that the patches deserve a human look before they land upstream.

Beyond fuzz tests

The OSS-Fuzz project is the headline, but the post describes several other experiments. Claude wrote a formal specification of RFC 1950, the zlib data format, and proved that the zlib implementation in the Linux kernel follows it. This time it worked on the x86 binary, using x86 semantics that Claude generated itself. The team repeated the exercise for half a dozen other widely used libraries and found only minor, unexploitable corner case bugs, which suggests that these heavily tested codebases are already nearly correct.

Claude also built an interpreter for a large subset of Python in Rust and proved with the Verus tool that it follows CPython semantics from an academic paper. In a test with more than 1.7 million random Python programs, it matched CPython in 99.95% of cases. In another effort aimed at a widely used PDF reader, the team says it found as many security bugs in one week as are usually reported in a year.

Getting cheaper fast

The biggest practical limit today is cost. Anthropic says a proof can take hundreds of millions of tokens. Two findings suggest that will fall. On a set of 36 small verification tasks built from real OSS-Fuzz code, Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. And when agents were allowed to copy each other's finished proofs in a shared workspace, they needed 17% fewer tokens than agents working alone. Most of any proof covers code every program contains, such as C runtime and sanitizer start up, so proofs are highly reusable.

That is the core of Theorem's bigger plan. In a September post the company laid out a roadmap for verifying the Nix package ecosystem from the bottom up, starting with shared libraries like glibc, OpenSSL and curl, because once a dependency is proven, everything built on top of it can reuse that proof. Its own OSS Verify program now offers the pipeline free to qualifying open source projects. Maintainers open a pull request with a project file, a Dockerfile and a build script, receive a Rocq proof per fuzz target, and get any bugs reported privately with no disclosure deadline. Theorem says proofs can take several days and that widely used critical infrastructure gets priority. The repository includes a Claude skill that walks a coding agent and a maintainer through enrollment.

What it does not prove

The authors are unusually direct about the limits, and they matter:

• The model is not the machine. The proofs cover single threaded, static RISC-V binaries linked against musl libc. Most people run these libraries on x86 or ARM with glibc and dynamic linking.
• The claim is not everything. AddressSanitizer does not catch every memory safety bug, not every entry point of each library was proven, and even all entry points would not cover a whole library.
• Callers can still misuse a library. A proven parser does not protect a program that calls it wrong.
• The trusted core can be wrong. If the RISC-V or Linux models differ from reality, the proof may not match the real world.

Our take

This is one of the more consequential AI security results of the year, and not because of the 180 million lines. The important shift is in the economics. Formal verification used to be a boutique service for a few critical systems. If a model can take tests that maintainers already wrote and turn them into machine checked guarantees in days, verification starts to look like fuzzing did fifteen years ago: an expensive research idea about to become routine infrastructure.

The honest framing is the one Anthropic uses itself. These are strong but narrow guarantees about specific entry points under a specific machine model, and the trusted core still needs scrutiny. But the method points in the right direction. The same capability that lets AI find bugs at scale can also prove their absence at scale, and only one of those two leaves defenders ahead. If you maintain a parser, a decoder or a compression library, OSS Verify is worth a look today.

Sources: Anthropic: LLMs are making formal software verification feasible at a much larger scale, Theorem: OSS Verify, Theorem: Bootstrapping the Verified Software Stack, Theorem on GitHub: oss-verify-proofs, Unite.AI: Anthropic Says Claude Proved Security Properties Across 123 Libraries.