Proven, not tested: AI now checks software by proof. What it means for your products

TL;DR. On October 22, Anthropic and the company Theorem showed that Claude can do more than test software: it can check it by mathematical proof. For 123 widely used open-source libraries there is now a machine-checked proof that certain parts of the code do not crash on any input below 64 MB. Along the way, hundreds of bugs came to light, one of them more than ten years old. The proof, however, holds for a test environment, not for the machines your software runs on. Formal proofs are becoming affordable. If you test software today, set up your tests so they can be proven tomorrow.

What is new: proof instead of sampling

Security-critical libraries are mostly checked with random tests today. In so-called fuzzing, a program throws millions of random inputs at the code and waits for a crash. Google's OSS-Fuzz project does this for 1,381 open-source projects. It remains a sample: whatever the tests miss stays undetected.

Anthropic's Frontier Red Team describes the next step in its post of October 22. Claude turned existing fuzz tests into formal statements, for example: this program does not crash on any input below 64 MB. Then it proved those statements, for the compiled program, not just the source code. An independent checker called Rocq verifies every step. After a few weeks there were 239 entry points in 123 libraries, about 180 million lines of proof in total. Along the way, Claude found hundreds of bugs that had gone undetected for years despite trillions of test runs, and fixed them. One logic bug had been in the code for more than a decade.

A small experiment in the appendix shows how big the difference is. The team deliberately planted seven bugs in a Python interpreter that Claude had written and proven. Five of them survived the random tests. All seven broke the proof.

Why hardly anyone did this before

Formal proofs have existed for decades, for flight control software for example. But they were so laborious that they rarely appeared anywhere else. The effort is still huge, only now the machine carries it. For the 391-line parser of the cJSON library, Claude wrote a proof of 630,000 lines. Only about a tenth of it concerns cJSON itself. The rest proves start-up code, memory management and the checking tools along with it. In total, Claude wrote about one billion lines, of which 180 million ended up in proofs that passed the check.

According to Anthropic, a single proof takes hundreds of millions of tokens. The post does not give a price. Checking a finished proof takes 30 minutes to several hours of compute time. But the curve points down: Opus 5.5 solves half of 36 proof tasks with about 40% fewer tokens than Opus 5. When several agents work in a shared proof workspace, they save another 17%.

The catch

• Proven for a test machine, not for your servers. The proofs hold for single-threaded, statically built programs on the RISC-V processor architecture with the musl C library. Most servers and computers run on x86 or ARM with glibc.
• No crash does not mean correct. What is proven is that certain kinds of errors do not occur. A wrong result is not ruled out. Anthropic itself writes that formally verified does not mean bug-free. In the Hacker News discussion (442 points) this was the most common objection: a proof only shows what the statement says.
• The AI could cheat. Claude could have changed a program so that it becomes easy to prove. The team penalized such changes, logged them and audited them.
• Open whether it scales. In the appendix, the team concedes that other projects using this verbose proof style hit a complexity wall. Larger programs probably need better building blocks.
• Only part of it can be checked publicly. Theorem's archive so far holds proofs for 25 libraries. Anthropic is holding back proofs that could reveal bugs that are not yet fixed.

Our analysis: where do industrial libraries stand?

At launch, Theorem published a public index. It states checkable claims for 427 of the 1,381 OSS-Fuzz projects, 20,164 in total. 138 of them are proven, or 0.7%. On October 24 we looked at the libraries that sit inside machines, plants and networks.

For OPC UA, the most important standard for data exchange on the factory floor, 224 statements are ready and none is proven. For the energy systems standard IEC 61850 there are 116, also without a proof. Modbus cannot even be described by the model yet. For OpenSSL, 12 of 442 statements are proven. So the tools are ready, but the work on industrial software has only just begun.

What it means for mid-sized companies

Most mid-sized companies do not write compression or encryption libraries. But they build them in, into machine controllers, gateways, web portals and apps. Since September 11, 2026, manufacturers of such products must report actively exploited vulnerabilities within 24 hours under the Cyber Resilience Act. From December 2027, the remaining obligations apply. A kind of error that has been proven impossible before shipping will not lead to a report later.

The route Anthropic took matters: every proof started from an existing fuzz test. If you have no tests today, you will have nothing to prove tomorrow. Anthropic expects formal proofs to soon be as practical for almost all software as fuzzing is today. Whether it happens that fast is open. The direction is not.

What you should do now

1. Know what is inside. Keep a bill of materials of the libraries (SBOM) for every product that contains software. The Cyber Resilience Act requires it anyway.
2. Install updates. The bugs found are being fixed in the libraries themselves. The fixes only reach you if you update.
3. Test parsers first. Code that reads files or network data from outside is the way in for attackers. Give it fuzz tests. That is good practice today and the precondition for a proof tomorrow.
4. Ask suppliers precisely. When a vendor promises "formally verified": what exactly is proven, for which platform, and what do you have to trust?
5. Do not drop testing. A proof only covers what the statement says. For everything else, tests remain necessary.

Until now, formal proofs were handwork for a few specialists. Now they are becoming a compute job, still expensive and narrowly scoped, but with falling costs. If you want to know which libraries sit inside your products and where tests are missing, we are happy to take a look together.