AI Formal Verification Now Turns Fuzz Tests Into Proofs. Here's What They Actually Cover

Claude proved 239 fuzz tests across 123 libraries crash-free. The proof is real, and so is the narrow build it assumes.

A fuzzer can run for a year and never tell you your code is safe. It throws millions of random inputs at a program and reports the ones that make it crash. When it finds nothing, all you learn is that it found nothing.

There has always been a stronger answer, and almost nobody could afford it. Formal verification means writing a mathematical proof that a program behaves correctly for every possible input, then having a strict checker confirm each step. The famous example, the seL4 microkernel, took about 20 person-years to verify against roughly 2 to build, according to Anthropic's own background figures. So proofs stayed in aerospace, kernels and research papers.

That changed shape on October 22. Anthropic's Frontier Red Team, working with collaborator Theorem, published results where Claude wrote proofs that 239 entry points across 123 open-source libraries "will always exit normally without triggering memory-safety errors or failing assertions." The proofs cover every input smaller than 64 MB. The team calls it "the first large-scale effort to use AI to apply formal verification to production software."

Here is the idea worth holding onto. A proof is only as wide as the question it answers. This one answers a precise, narrow question very well. If you build or ship software, the useful skill now is reading that question before you repeat the headline.

What they actually did

Start with something most C and C++ maintainers already have: fuzz tests. Projects in Google's OSS-Fuzz program ship small harness functions that take a blob of bytes and feed it to the library. A fuzzer calls those functions with random bytes, looking for crashes.

The team reused those harnesses as questions. For each one, they compiled the entry point down to RISC-V machine code (the low-level instructions a CPU actually runs) and generated a theorem: this program will not crash for any input under 64 MB. "Crash" here means a memory-safety error caught by AddressSanitizer (a compiler tool that flags out-of-bounds reads and writes) or a failed assertion.

Then Claude wrote the proof, and Rocq checked it. Rocq is a proof checker, formerly called Coq. Think of it as a referee with no imagination: it accepts a proof only if every single step follows from the rules, so a confident-sounding wrong argument gets rejected the same way a compiler rejects a typo.

The scale is the news. The proofs total about 180 million lines of Rocq. A typical one runs around 600,000 lines, for binaries with a median of 18,000 RISC-V instructions. Nobody reads those by hand, and nobody has to, because the checker does.

Why machine code instead of the source? The post says working at the binary level lets the method avoid "rewriting entire codebases in another language," and it means the proof talks about what the compiler actually produced, not what the source looks like it should do.

What happened when a proof failed

The interesting part is the failures. When Claude could not prove a target safe, the reason was often a real bug. Claude patched the code and proved the patched version. The post says the team found hundreds of bugs this way, and the examples read like a list of things fuzzers miss:

• A counter underflow in a decompressor that led to an out-of-bounds write, but only on roughly 20 MB inputs with one rare layout.
• An image decoder with an out-of-bounds read that needed a 64 MB input and over 2 GB of memory.
• An out-of-bounds read that only appeared after a specific sequence of calls across two handles to the same file.
• A rediscovery of a known libexpat vulnerability that needed deeply nested input.

Look at the pattern. Twenty megabytes with one rare layout. Sixty-four megabytes and two gigabytes of RAM. Random fuzzing rarely wanders that far. A proof has to account for every input, so the strange corners come up whether anyone guessed them or not.

The team also ran side experiments. Claude wrote a formal spec of RFC 1950 (the zlib data format) and proved the Linux kernel's zlib implementation meets it. It built a Rust interpreter for a large subset of Python that matched CPython on 99.95% of 1.7 million random test programs. And during work on "a widely used PDF reader," the team says it "found as many security bugs in one week as are typically reported in a year."

Two cost notes from the same post. Agents that could copy each other's proofs from a shared workspace needed 17% fewer tokens than agents working alone. And on a 36-task benchmark, Opus 5.5 proved half the tasks with about 40% fewer tokens than Opus 5. The post also says single proofs "can take hundreds of millions of tokens," so cheap is relative.

What the proof does not cover

This is where most coverage will get sloppy, and where the post itself is careful. The authors write that "Formally verified" does not mean "bug-free," and they list why.

The build is not your build. The proofs assume a single-threaded, statically linked (everything bundled into one file) RISC-V binary using the musl C library, running under Linux with a fixed memory budget. Most people run these libraries on x86 or ARM, dynamically linked against glibc (the standard C library on most Linux systems). The proof says nothing directly about that program.

The question is "no crash," not "correct." AddressSanitizer does not catch every memory-safety bug. A library that returns the wrong answer without crashing passes. The post gives an example: a file-restriction feature that was not always enforced, a logic bug that never crashes.

Only the fuzzed paths count. Not every entry point was verified, and code no fuzz test reaches is not covered. If your harness never calls a function, the proof never mentions it.

Callers can still break things. A program that misuses the library, say by passing a freed pointer, can still corrupt memory. Covering that needs a separate spec for each function's callers.

The referee has to be right too. Rocq, Theorem's model of RISC-V and Linux, the hardware, the OS and the OCaml compiler under Rocq are all trusted. A bug in any of them weakens the result.

The model can cheat. A footnote warns that Claude could make a theorem provable by rewriting the program so it never crashes, for example by making it exit early on anything difficult. The team penalized patches, offered extra credit for showing exactly which inputs a patch changed, and audited the patches.

None of this makes the work less impressive. It makes it specific. A proof that a static musl RISC-V build of libexpat cannot crash on inputs under 64 MB is a strong, useful fact. It is not the sentence "libexpat is safe."

Why your fuzz tests just became more valuable

Here is the shift for builders. The team did not write 239 specifications from scratch. They reused fuzz harnesses that maintainers had already written for a different purpose.

That turns every fuzz target into a spec an AI can prove against. A project with good harnesses that reach deep into the parser is now one enrollment away from proofs. A project with one shallow harness gets a proof about one shallow path. A project with none gets nothing.

It also changes how to read a security claim. Expect "formally verified" to show up in vendor decks and README badges soon. The question to ask is the same one this article keeps returning to: verified for which build, which entry points, which property, and which inputs?

Put this into practice

1. If you maintain a C or C++ library with fuzz targets, look at OSS Verify. Theorem runs the pipeline as a program called OSS Verify. The fast path is to paste one instruction into a coding agent started in your project checkout; the agent reads the program's AGENTS.md, asks you what "correct" means for your code, and sets up a projects/<name>/ folder. The manual path is two commands after you create that folder from the templates:

tools/validate.py projects/<name>
tools/check --no-shell --twice <name>

The second command builds every fuzz target twice and confirms the two builds are byte-identical, so the proof is pinned to an exact binary. You then open a pull request. After merge, the service proves theorems about the binaries and sends findings privately to your security contact, with patches when it has them.

What you need, per the README: Linux x86-64, Docker, git, Python 3 with PyYAML, about 10 GB of free disk, a public repository, a security contact and at least one fuzz target. The first run downloads a toolchain image of about 1.1 GB.

2. Read the two warnings before you run it. tools/check builds your project's Dockerfile with network access, so the README says to run it only on a project you trust. And findings and patches are AI-generated and "may be wrong or incomplete." Review every patch like a pull request from a stranger.

3. If you have no fuzz targets, write one this week. It is the entry ticket now. Pick the function that parses untrusted input (a file format, a network message, a config) and write a harness that feeds it raw bytes. Aim it at the deepest code you can reach, because the proof will only be as wide as the harness.

4. Use a four-question checklist on any "verified" claim. Which binary (architecture, libc, linking, threads)? Which entry points? Which property (no crash, or actually correct)? Which input bound? If a vendor cannot answer all four, the claim is marketing.

5. Look at the published artifacts. Anthropic released a subset of the proofs (theorem-labs/oss-verify-proofs, whose README lists 60 entry points in 25 libraries, checked with Rocq 9.2.0) and the RISC-V and Linux semantics (theorem-labs/rocq-linux-process-semantics) so anyone can check or reuse them. Proofs that might reveal unpatched bugs are held back.

Honest limitations

The method is narrow today. The build model is not what most people deploy, and the post says so.

Enrollment has gates. The OSS Verify README asks for an OSI-approved license and a core maintainer to enroll, so you cannot point it at a dependency you merely use.

The token bill is large. "Hundreds of millions of tokens" for some proofs means this is a service someone else runs, not a CLI you fire off on every commit.

Every number in this piece comes from Anthropic and Theorem. The proofs are checkable, which is the point of Rocq, but the bug counts, the 99.95% interpreter match and the PDF-reader comparison are the team's own reports.

And the hardest problem is upstream of the AI. A proof answers the question you asked. If the harness asks a shallow question, you get a deep answer to it.

Where this leaves you

For decades the honest answer to "can we prove this is safe?" was "not at a price you will pay." For the narrow question of "will this fuzz target crash," that answer just changed for a lot of open-source code.

Spend the next hour on the part you control. Check whether your library has fuzz targets, check how deep they reach, and decide whether a proof about that build is worth having. Then, the next time someone tells you their code is formally verified, ask them which build.

Sources: Anthropic, "LLMs are making formal software verification feasible at a much larger scale" (October 22, 2026) · theorem-labs/oss-verify README · theorem-labs/oss-verify-proofs · theorem-labs/rocq-linux-process-semantics. Reviewed October 23, 2026; OSS Verify had no tagged releases.