LLMs and formal verification: what "proved" means for 123 libraries

On October 22, 2026, Anthropic's Frontier Red Team, working with a company called Theorem, published a result worth reading slowly. They used Claude to write formal proofs for real open-source code at the assembly level, across 123 libraries, and found bugs along the way that had survived years of testing. Here is what that means in plain words, where the word "proved" stops, and what a normal team can take from it today.

Formal verification, without the jargon

A test checks the inputs you thought of. A proof covers every input. In formal verification you turn code into a mathematical model, write down rules it must always follow, and try to prove the model follows them. If the proof fails, the way it fails points at a possible bug. Fix it, try again, and you end with a proof that no bug breaking those rules is left.

The catch has always been cost. The post gives the classic example: the seL4 kernel took two person-years to build and 20 person-years to verify. So verification stayed in places like avionics code.

What they actually did

Writing a specification is usually the hard part, so they reused one that already existed: fuzz tests from Google's OSS-Fuzz. A fuzz test is an entry point that crashes when something is wrong, and a fuzzer throws huge numbers of generated inputs at it. It can run for years and still never be complete. The team turned each fuzz test into a statement: this entry point never crashes, for any input under 64 MB, on the compiled RISC-V binary.

Over a few weeks, Claude patched the bugs it hit and proved that statement for 239 entry points across 123 libraries. The proofs total about 180 million lines of Rocq; a typical one is about 600,000 lines, for binaries with a median of 18,000 RISC-V instructions. Nobody reads that by hand. The Rocq proof checker does, and the post lists what you still have to trust: the formal models of RISC-V and Linux processes, the exact theorem statements, and the checker itself.

The bugs are the part to notice

Fuzzers mutate small inputs, typically capped at 1 MB. Some of what the proofs turned up sits far outside that: a counter underflow in a decompressor that caused an out-of-bounds write only on inputs around 20 MB with one rare layout, an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory, and a rediscovery of CVE-2026-56132 in libexpat. One proof also exposed a logic bug that never crashes: a feature for restricting which files an application can load was not always enforced. The authors' point is that just attempting the proof finds real bugs, whether or not it finishes.

Where "proved" stops

The post is direct about this, and I think it is the most useful section. "Formally verified" does not mean "bug-free". It means the code follows the rules that were written down, on the machine that was modelled. Two gaps it names:

• The machine. The proofs are about single-threaded, static RISC-V binaries linked against musl. Most people run these libraries on x86 or ARM, dynamically linked against glibc.
• The claim. AddressSanitizer does not catch every memory bug, not every entry point was verified, and a caller can still misuse the library.

What this means for an ordinary team

You are probably not about to write Rocq. But the method here starts from something many teams already have: a test that states a property. A fuzz harness that crashes when a round trip fails is a specification in disguise, and the post notes that proving such a test never crashes is the same as proving the property. A small example of the shape, illustrative and with placeholder function names:

#include <assert.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

/* your library's own functions; the names are placeholders */
size_t encode(const uint8_t *in, size_t n, uint8_t **out);
size_t decode(const uint8_t *in, size_t n, uint8_t **out);

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  uint8_t *packed = NULL, *back = NULL;
  size_t packed_n = encode(data, size, &packed);
  size_t back_n = decode(packed, packed_n, &back);
  assert(back_n == size && (size == 0 || memcmp(back, data, size) == 0));
  free(packed);
  free(back);
  return 0;
}

Writing tests like this, where a failure means a stated rule was broken, is useful today with a plain fuzzer, and it is exactly what this kind of tooling can later turn into a proof. Theorem says it is offering to run the same pipeline for other open-source projects and is publishing a Claude skill to help developers start verifying their own code.

Next step: pick one parser or encoder in your codebase and write the property it must always keep as a test that fails loudly. Then read the limitations section of the original post before you trust any "formally verified" label. Source: Anthropic Frontier Red Team, LLMs are making formal software verification feasible at a much larger scale.