• Claude wrote about 180 million lines of Rocq proofs covering 123 open-source libraries and 239 entry points, and a separate proof checker validated them.
• The proved property is no-crash on inputs under 64 MB, derived from existing fuzz harnesses. It is not full functional correctness.
• The proofs assume a single-threaded static RISC-V binary linked against musl libc. Typical x86 or ARM glibc deployments are not modeled.
• Anthropic reports hundreds of bugs, including some that survived trillions of fuzzing runs. This is a vendor report with no independent replication yet.
• Binding now: nothing. Binding soon: a procurement question about whether 'formally verified' claims state the machine model and spec.

Anthropic reports that Claude generated roughly 180 million lines of Rocq proof code showing that 123 open-source libraries do not crash on inputs under 64 MB, and that the work exposed hundreds of bugs, some of which had survived trillions of fuzzing runs. The scale is new. The guarantee is narrower than the headline suggests, and every figure here comes from the vendor's own post, not from independent replication.

What was demonstrated

Claude proved a no-crash property, not correctness. According to Anthropic, each library's existing fuzz test was compiled to RISC-V, its no-crash property was turned into a formal specification, Claude wrote the proof, and Rocq checked it. The post cites 239 entry points, a median binary of 18,000 instructions and about 600,000 lines for a typical proof. The model's output is untrusted by design: only the checker's verdict counts.

Why the bug finds matter

Proofs reached code that fuzzing had not, which is the substantive finding. Anthropic says some bugs survived trillions of test runs, that a widely used PDF reader yielded as many security bugs in one week as are typically reported in a year, and that one logic error had been latent for over a decade. Claude also patched what it found and re-proved the fixed code, with patches penalized and audited to discourage gaming the spec.

Where the guarantee stops

The proofs hold only under stated assumptions. Anthropic says they assume a single-threaded, static RISC-V binary linked against musl libc, running under a fixed memory budget on Linux. Trusted components include the Rocq checker, the RISC-V and Linux models, the hardware and the OCaml compiler. Production systems commonly run x86 or ARM with dynamic glibc, which are not modeled, and callers that misuse a library stay outside the proof.

What has not been verified

No outside party has reproduced these results. The Decoder restates Anthropic's figures, and the primary post is the only detailed source. Anthropic also says not every entry point was verified and dead code is uncovered, and notes that its AddressSanitizer checks do not catch every memory-safety bug. Proofs can consume hundreds of millions of tokens, and total project cost was not reported, so the economics remain unknown.

What to do with it

Treat this as a lead and a procurement question, not a certification. Nothing is binding now. Soon, expect vendors to say 'formally verified' about AI-generated artifacts. Ask for the specification, the machine model, the trusted base and the proof artifacts, then check them against your build. If your libraries run on x86 glibc, the RISC-V proof describes a different binary from the one you ship.