Claude used to mathematically verify compiled RISC-V code, and flagged x86 chip flaws

What the team says it did

As SmartHey reported, Anthropic's frontier red team (its in-house group that stress-tests its own models) worked with Theorem Labs. They used Claude to run formal verification on real RISC-V programs. RISC-V is an open standard for processor instructions, and the work targeted compiled machine code, not the human-readable source.

Formal verification means proving mathematically that a program cannot do certain bad things, such as crash or read memory it should not. The proofs were written by Claude and then checked by Rocq, a tool that rejects any flawed step. That check is what makes AI-written proofs trustworthy.

Why proofs beat random testing

The standard security method is fuzzing, which throws huge numbers of random inputs at a program to see if it breaks. It is probabilistic, so a bug that only triggers on one very specific, large input can hide even after trillions of tries.

The proof approach turns each program entry point into a claim: for any input up to a stated size, nothing undefined can happen. If a proof stalls, the stall points at the likely bug. Claude can then draft a fix and rerun the proof.

In a test with seven planted bugs, random testing found two. Formal verification found every one. On a popular PDF reader, Claude reportedly found in one week as many flaws as the software's public security reports had listed in a year.

The cost of rigor and the x86 surprise

The proofs are enormous. A small JSON parsing library has a short entry point, yet its proof is far longer, because it must model program startup, memory handling and system calls. Only about a tenth of it concerns the library's own logic.

Claude also reportedly built a full mathematical model of the x86 instruction set. In the process it found hundreds of contradictions or errors in official x86 documentation and a logic flaw in a CPU itself.

The report says costs are falling as proof pieces get reused. It puts one end-to-end check of OpenSSL, a widely used encryption library, at a few hundred thousand dollars, but only a low double-digit dollar figure per package when spread across the packages that depend on it.

What to treat with caution

Our material is one outlet's summary. The headline's phrase about reaching the x86 hardware flaw layer is vivid, but we have not seen the report, and the CPU flaw is not described in detail. Cost and growth projections are the team's own estimates.

A first batch of proofs is public on GitHub, so outsiders can reproduce and audit the work. That is the real test of these claims.