Claude Wrote Machine-Checked Proofs for 123 Libraries

Claude found a year's worth of security bugs in one widely used PDF reader in a single week. And that was a side note. The bigger news is that Anthropic had Claude write machine-checked proofs for real open-source software, at a scale that used to be out of reach.

What happened

On October 22, 2026, Anthropic published research on formal verification done with Theorem, which it calls its collaborator on the project. Here's what the post reports:

• Claude proved that 239 entry points across 123 open-source libraries from OSS-Fuzz have "no crashes on any input (up to 64 MB)."
• The proofs add up to about 180 million lines of Rocq, a proof language whose output a machine checks. A typical proof runs about 600,000 lines, for binaries with a median of 18,000 RISC-V instructions.
• Trying to write the proofs "discovered hundreds of bugs," which Claude patched. Some were in code fuzzers would rarely reach, such as a counter underflow that needed an input of around 20 MB.
• In one case study, the team found "a previously unknown logic bug that had been latent for more than a decade."
• While verifying a widely used PDF reader, they found "as many security bugs in one week as are typically reported in a year." The reader isn't named.

For scale, the post points to seL4, the verified operating system kernel: building it took two person-years, and formally verifying it took 20.

Theorem is offering to run the same pipeline for other open-source projects, and it's publishing a Claude skill to help developers verify their own code.

The limits, in Anthropic's words

This part matters as much as the headline. The post says "formally verified" does not mean "bug-free." A proof is only as good as its specification and its machine model. The proofs assume a single-threaded static RISC-V binary linked against musl libc on Linux, while most real users run x86 or ARM with glibc. Not every entry point was verified. The proofs don't cover callers misusing a library. And a single proof can take hundreds of millions of tokens to produce.

The accurate summary: 239 entry points are proven crash-free under a specific model, and hundreds of real bugs got fixed along the way. That's still remarkable.

Why it matters for builders

Formal proofs used to be something only a few specialist teams could afford, reserved for things like operating system kernels. The cost was people's time. If a model can do the heavy lifting and a machine checks every line, the cost turns into compute.

Even if you never write a Rocq proof, the workflow carries over. You state precisely what your code must never do, and the agent has to prove it or show you the input that breaks it. That's a much stronger check than "the tests passed."

Try it in 15 minutes

You can start thinking in specifications today with the tools you already have.

1. Pick one function in your codebase that parses untrusted input: a file upload handler, a URL parser, a config loader.
2. Ask Claude Code to write down, in plain English, the properties that function must always hold. For example: never crashes on any byte string, never reads past the buffer, always returns a value or a typed error.
3. Have it turn each property into a property-based test with Hypothesis for Python or fast-check for JavaScript, and run them.
4. Ask it to explain every failing case and propose the smallest fix.
5. If you maintain an open-source library, read Anthropic's post, check whether your project is in OSS-Fuzz, and look at Theorem's offer to run the pipeline on it.

Property tests are a long way from a full proof. They train the habit that makes proofs possible: a precise statement of what correct means.

Here's how you get paid

My opinion: proving code is safe used to take expert teams years. Now AI does a lot of the heavy lifting, and that opens a premium service for teams shipping critical code.

I'd call it a proof-backed security audit. Start with the property-based layer, which you can deliver now: write the specifications for a client's riskiest parsers and handlers, generate the tests, fix what breaks, and hand over a report that says exactly what was checked and under which assumptions. As tooling like Theorem's skill matures, add machine-checked proofs for the few functions where a crash would be catastrophic.

Be honest about limits in every report, the way Anthropic was. Clients in fintech, health and infrastructure will trust you more for it, and those are the clients who already pay for audits.