Claude beviste at 239 fuzz-mål i 123 OSS-Fuzz-biblioteker ikke kan krasje under 64 MB

Det tok to årsverk å skrive operativsystemkjernen seL4 og 20 årsverk å verifisere den formelt. Anthropic skriver denne uken at Claude, i samarbeid med verifiseringsselskapet Theorem, på noen uker beviste at 239 fuzz-mål i 123 biblioteker fra Googles OSS-Fuzz ikke krasjer for noen input under 64 MB. Bevisene utgjør rundt 180 millioner linjer Rocq og gjelder den kompilerte RISC-V-maskinkoden, ikke kildekoden.

Slik blir en fuzz-test et bevis

Anthropic slipper å skrive spesifikasjoner ved å gjenbruke fuzz-testene utviklerne allerede har. En fuzz-test krasjer når noe er galt, og AddressSanitizer (ASan) får programmet til å krasje ved ugyldig minnetilgang. Teoremet blir dermed enkelt: denne binærfilen krasjer aldri. Rocq-bevissjekkeren avgjør om beviset er gyldig, så det du må stole på er modellene av RISC-V og Linux-prosesser, selve teoremene og sjekkeren.

«Selv om dette er en enorm mengde beviskode, trenger praktisk talt ingenting av den å gjennomgås manuelt.» — Anthropic, i forskningsrapporten

Underveis dukket det opp feil som fuzzere sjelden treffer, fordi de typisk muterer input på maks 1 MB. En teller-underflyt i en dekomprimator ga out-of-bounds-skriving, men bare på input rundt 20 MB med et sjeldent oppsett. En bildedekoder hadde en out-of-bounds-lesing som krevde 64 MB input og over 2 GB minne, og Claude gjenoppdaget CVE-2026-56132 i libexpat, som krever dypt nøstet input. Claude patchet feilene selv og beviste deretter den patchede koden.

Begrensningene

Bevisene gjelder entrådede, statisk lenkede RISC-V-binærer mot musl libc. De fleste kjører de samme bibliotekene på x86 eller ARM med glibc, og der gjelder ikke garantien. ASan fanger heller ikke alle minnefeil, og bare noen av fuzz-målene i hvert bibliotek er bevist. Et appendiks til rapporten peker på et tredje problem: agentenes bevis er ordrike og staver ut registerinnhold og hver gren, der menneskelige bevisingeniører ville innført abstraksjoner. Erfaringer fra andre agentprosjekter tyder på at den stilen kan treffe en kompleksitetsvegg på større programmer.

Ett bevis kan kreve hundrevis av millioner tokens. Anthropic oppgir at Opus 5.5 løser halvparten av 36 små verifiseringsoppgaver med rundt 40 prosent færre tokens enn Opus 5, og at agenter som fikk kopiere hverandres bevis brukte 17 prosent færre tokens.

Prøv det på ditt eget prosjekt

Theorem tilbyr samme pipeline gratis for kvalifiserte åpen kildekode-prosjekter gjennom OSS Verify. Påmeldingen fungerer som i OSS-Fuzz: en pull request mot theorem-labs/oss-verify med project.yaml, Dockerfile og build.sh, og byggene må gi statiske riscv64-binærer. Bare kjernevedlikeholdere kan melde på et prosjekt, et bevis kan ta flere dager, og Theorem lover ikke at et menneske leser gjennom de KI-genererte funnene og patchene før de sendes.

«I stedet kan du nå få et bevis på at fuzz-testen din aldri vil finne en ny feil, uansett hvor lenge den kjører.» — Theorem, på OSS Verify-siden

Hva bør du gjøre?

1. Vedlikeholder du et C- eller C++-bibliotek som allerede ligger i OSS-Fuzz, start fra de eksisterende byggefilene og meld det på OSS Verify. Prosjekter med under 1 MB binær .text blir verifisert først.
2. La en kodeagent gjøre porteringen. Theorem har lagt ut Claude-skillen add-project, som intervjuer vedlikeholderen om hva «korrekt» betyr og skriver fuzz-målene.
3. Skriv fuzz-tester som sjekker egenskaper, ikke bare krasj, for eksempel at decode(encode(x)) gir x tilbake.