Claude churned out 180 million lines of proof, and all the bugs that had been missed in trillions of test runs were completely rooted out by AI in one go.

Are global software bugs about to be wiped out by Claude?

In just 48 hours, 27 major cyberattacks broke out across the globe, and people are now widely spreading the rumor that the "Darkest October" has arrived.

Earlier that day, Anthropic's cutting-edge red team joined hands with Theorem Labs to release a high-impact report —

They let Claude dive deep into low-level assembly instructions (RISC-V) to launch a full-scale attack on real production-grade open source code repositories.

In just a few weeks, Claude completed formal verification for 239 test entry points across 123 open source code repositories, generating a staggering 180 million lines of Rocq mathematical proof code that all passed machine verification!

Hidden vulnerabilities that even Google's platform failed to uncover after trillions of runs, high-risk logical dead ends that have lurked for more than a decade, and even real defects in the x86 processor hardware itself, all surfaced in this massive cleanup operation.

Even more notably, in one popular PDF reader, the number of security vulnerabilities Claude unearthed in a single week directly matched the total number of vulnerabilities it would normally report in an entire year.

This time, Claude integrated bug finding, bug fixing, and fix verification into a single workflow, launching a "mathematical-level" bug cleanup campaign.

The global sweeping cybersecurity crisis may finally get a viable solution.

Bugs Missed After Trillions of Tests

Forced to Surface by Mathematical Proof

Over the past decade, one of the most relied-upon defense lines in the open source world has been OSS-Fuzz, launched by Google in 2016.

This method, known as fuzz testing, feeds batches of semi-random inputs into program entry points to see which input can crash the program, and it has cumulatively run trillions of tests.

But fuzz testing is ultimately a game of chance in a maze. Its input is usually limited to less than 1MB, and as long as there is one untested execution path, bugs on that path can remain hidden indefinitely.

This time, the research team rewrote the test entry point into a mathematical proposition, stating that under set conditions, any input smaller than 64MiB will not trigger the agreed crash, including assertion failures and errors that can be captured by the ASan memory detection tool.

Claude's task is to prove this proposition. A single successful run does not count. Every possible input and every reachable execution path within the specified range must be proven not to trigger the above errors.

When the proof gets stuck, either Claude has not found the proof method yet, or there is indeed a bug in the program. After finding the bug, Claude will automatically generate a patch and continue the subsequent proof process.

As a result, those bugs hiding in corners unreachable by traditional tests surfaced.

A counter underflow hidden in a certain decompressor would write data beyond the memory boundary, but it can only be triggered by input of about 20MB with a very rare arrangement pattern.

The research team stated that the process of attempting to prove alone has uncovered hundreds of bugs.

To compare the difference between testing and formal proof, the researchers deliberately embedded 7 bugs in a Python interpreter written by Claude in Rust.

Random testing let 5 of them slip through, while the formal proof caught every single bug without exception.

391 Lines of Code, 630,000 Lines of Proof

This batch of proofs is implemented at the lowest level.

The object of Claude's proof is the RISC-V machine code that actually runs on the CPU after compilation. The source code and the compiled program are not necessarily completely consistent. Only by proving down to the machine instructions can the proof cover the actual running program.

To achieve this, Theorem first wrote mathematical models for RISC-V instructions and the behavior of Linux processes. The current proof is built on this set of models, limited to an environment with single thread, static linking, and fixed memory budget.

Proving down to this level leads to a surge in engineering volume. A parsing entry point of the JSON parsing library cJSON only has 391 lines of C code, and Claude wrote 630,000 lines of Rocq proof for it.

The volume expands by a thousand times because the proof needs to cover the entire process. The startup of the C program, the memory allocator, printf, and the runtime of the memory detection tool itself all need to be proved together, and only one-tenth of the proof content is directly related to cJSON itself.

Across the entire project, Claude cumulatively wrote about 1 billion lines of proofs, of which about 180 million lines finally passed the inspection. More than half of these proofs are automatically generated by tools written by Claude itself.

The final gatekeeper is the Rocq proof checker, which verifies step by step according to logical rules, and a single proof takes 30 minutes to several hours of CPU time. The checker confirms that the proof complies with specifications, and humans still need to review whether the specifications and machine models correspond to real requirements.

No matter how smooth the model is written, if it cannot pass the checker, none of the lines count. Writing proofs of such a scale was an unthinkable amount of engineering in the past.

For the legendary microkernel seL4, writing the code only took 2 person-years, but completing formal verification for it took a full 20 person-years. Therefore, for decades, this level of security guarantee was only affordable for mission-critical code such as Airbus flight control systems.

But this time, Claude completed verification for 123 open source libraries in only a few weeks.

Claude Wrote a Full Set of Mathematical Models for Chips

And Uncovered Hardware Bugs Along the Way

To see how deep Claude's proof can dig, you only need to look at cpp-httplib.

To rule out the possibility of stack memory overflow caused by excessively deep recursion, Claude traced into the red-black tree in the C++ standard library libc++, and proved on machine code that the height of this tree is always maintained at a logarithmic level. Only when the height of the tree is controlled, the number of recursion layers during destruction has an upper limit, and then it can be further proved that the stack space will not be exhausted.

It first wrote the formal specification for the zlib compression format standard, and then proved that the zlib implementation built into the Linux kernel fully conforms to this specification.

This time, the proof is implemented on x86 machine code, and the mathematical model of the x86 instruction set was completely independently written by Claude.

How accurate is this model? By stepping through each instruction one by one in the model, it can fully boot up the Ubuntu user space on the Linux kernel.

During the process of writing the model, Claude found hundreds of errors in the official x86 reference documentation, and also discovered a small number of bugs hidden in the CPU hardware itself.

From software all the way down to chips, AI is already helping humans recheck the entire foundation of computers.

Proof Speed Doubles Every Two Months

A $134 Million Verification Roadmap

The biggest threshold for formal verification is its high cost, and a single proof often consumes hundreds of millions of tokens. Nowadays, this cost is decreasing extremely rapidly.

Anthropic conducted tests with 36 small verification tasks. Opus 5.5 requires about 40% fewer tokens to complete half of these tasks than Opus 5.

Theorem tested 7 cutting-edge models released from May to September this year, and found that the verification speed roughly doubles every two months.

Moreover, proofs are reusable.

After the agents share the workspace, the same set of tasks consumes 17% fewer tokens. Projects that are seemingly unrelated such as libcups, freerdp, and libzmq share underlying code such as runtime libraries, so large sections of proofs are copied from pre-verified parts of other projects and modified for their own use.

Following this line of thinking, Theorem calculated the total cost using the Nix software ecosystem as a sample.

In the Nix software ecosystem, as long as 9MB of shared basic libraries cover all dependencies of two-thirds of machine code. The OpenSSL library alone appears in the runtime dependencies of nearly 16,000 software packages.

At