Today · research post October 22

Claude proves 239 entry points crash-free; Anthropic says so

Anthropic writes that Claude proved 239 fuzz-testing entry points in 123 open-source libraries can't crash on any input up to 64 MB. The proofs cover single-threaded static RISC-V executables only. Fuzz testing throws large volumes of random input at a program to find inputs that make it crash. Anthropic and its partner Theorem rewrote these tests as statements to prove: no input can trigger a crash. A proof covers every input by mathematical derivation, while testing shows only that the inputs tried didn't fail. Anthropic's post: "Claude successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries." (Anthropic, 2026-10-22). The conditions: each program runs as a single-threaded static executable with a fixed memory budget on RISC-V Linux. The proofs run to about 180 million lines and are checked mechanically by the proof checker Rocq rather than by human review. Anthropic writes that what remains to be trusted is the formal model of RISC-V and Linux processes, the statements themselves, and Rocq. Anthropic also writes that this doesn't mean the libraries are bug-free. The proving process turned up hundreds of bugs, which Claude patched before proving. The cost is hundreds of millions of tokens of proof work. All the figures are Anthropic's own, and Anthropic has published some of the proofs for independent checking. Our read: this kind of proof names exactly which components must be trusted. The property proved is "doesn't crash," not "does the right thing." How we checked →

Concept illustration in a black frame: on the left, a dark laptop with its lid lettered FUZZING sits beside a heap of small beige squares that arc up to a tall cream window panel in the centre, with three dots on its top bar and grey text lines, set against a pale pink circle. From the panel's base, red zigzag-folded strips printed with dark lines run across the table to a dark laptop on the right lettered CLAUDE, and a light plate at the bottom right reads ANTHROPIC, followed by a small mark.

Source and checks

This item ran in the brief of Oct 23, 2026, alongside 6 other items. How we checked it, the quote checks and what was still missing that day are on that issue's How we checked page.

Cite this item

SecondSource (2026). "Claude proves 239 entry points crash-free; Anthropic says so." https://secondsource.io/en/research/2026-10-23-1/. Accessed access date.