What the study reports
In an October 22 research report, Anthropic and Theorem say Claude produced Rocq-checked proofs for 239 fuzz-test entry points across 123 OSS-Fuzz libraries, sometimes after patching code. The stated target was no crashes on inputs under 64 MB in a defined execution environment. This is catch-up coverage of that report, not a new model release.
The study assumes single-threaded, statically linked RISC-V/Linux binaries and a fixed memory budget. Those builds do not automatically represent the x86 or ARM, dynamically linked software a team actually deploys.
Separate the study from the public artifacts
The public proof repository’s README inspected for this briefing lists proofs for 60 entry points in 25 libraries. It describes agreement between plain and sanitizer-instrumented compiled binaries under stated limits. It explicitly says the released proofs do not establish that a program halts. This public subset differs from the full reported campaign.
The theorem statement, machine and operating-system models, and Rocq checker remain trusted components. Crash checks do not cover every possible bug, every library entry point, or misuse by calling software.
Our take
For experienced technicians, a useful review starts with four questions: which property, which exact build, which environment, and how can the check be repeated? A machine-checked result can strengthen a release decision when its assumptions match the target. Keep integration tests and review of what the specification leaves out.
We inspected public source material. We have not executed the proofs, reproduced the study, or independently audited the checker.