Hva som faktisk ble bevist
Anthropics Frontier Red Team la 22. oktober fram resultater, sammen med Theorem, fra et forsøk på å bruke Claude til formell verifisering i stor skala. Laget tok eksisterende fuzztester fra Googles OSS-Fuzz, behandlet hver test som en egenskap koden må oppfylle, kompilerte den til RISC-V-assembler og lot Claude skrive maskinkontrollerte bevis for at den resulterende binærfilen aldri krasjer.
Egenskapen er snever og presis: for enhver inndata under 64 MB krasjer programmet ikke med en minnesikkerhetsfeil eller en mislykket påstand. Bevisene forutsetter en enkelttrådet statisk binærfil med fast minnebudsjett på en RISC-V-prosessor under Linux, og de stoler på beviskontrolløren Rocq, Theorems semantikk for RISC-V og Linux-prosesser, og maskinvaren og OCaml-kompilatoren under.
Tallene
I 123 åpne biblioteker beviste Claude at 239 inngangspunkter er fri for krasj under den spesifikasjonen. Bevisene utgjør til sammen rundt 180 millioner linjer Rocq. Et typisk bevis er omkring 600 000 linjer, mot en medianlengde på rundt 18 000 RISC-V-instruksjoner i binærfilen. Arbeidet tok noen uker.
Anthropic oppgir ikke hvor mange inngangspunkter som ble forsøkt totalt, så tallene gir ingen treffrate. Selskapet sier det publiserer bevis for de fuzztestene som ikke trengte noen rettelse, og spesifikasjoner for dem det ikke klarte å bevise.
Hundrevis av feil dukket opp underveis, og Claude rettet dem, noe som genererte spesifikasjonene på nytt. Eksemplene omfatter en tellerunderflyt i en dekomprimerer som gir en skriving utenfor grensene bare ved en sjelden oppstilling på rundt 20 MB inndata, en lesing utenfor grensene i en bildedekoder som krever 64 MB inndata og mer enn 2 GB minne, og en gjenoppdagelse av CVE-2026-56132 i libexpat. Én var en filrestriksjon som ikke alltid ble håndhevet: en logikkfeil som aldri krasjer, og som hadde ligget latent i mer enn ti år.
Den åpenbare snarveien, og hva de gjorde med den
Oppsettet har et hull laget selv peker på. Claude kunne gjøre et teorem beviselig ved å skrive om programmet slik at det aldri krasjer. Anthropic opplyser at selskapet straffet rettelser som endret atferd, ga ekstra uttelling for å bevise hvilke inndata en rettelse endrer, og loggførte og reviderte hver rettelse.
Kostnaden er det åpne problemet
På en test med 36 små verifiseringsoppgaver bygget av ekte OSS-Fuzz-kode, med tre uavhengige forsøk og et budsjett på fem millioner tokener hver, beviste Opus 5.5 halvparten med rundt 40 prosent færre tokener enn Opus 5. Agenter som fikk kopiere hverandres bevis fra et delt arbeidsrom, brukte 17 prosent færre tokener og fullførte 34 av de 36, mot 32 for agenter som arbeidet alene.
Anthropic er tydelig på begrensningene. «Formelt verifisert» betyr ikke feilfri: en beviskontrollør kan ikke bekrefte at spesifikasjonen svarer til virkeligheten, og feil kan bli igjen i spesifikasjonen, maskinmodellen eller den betrodde basen. Bevisene dekker RISC-V-binærfiler lenket mot musl, mens de fleste installasjoner kjører x86 eller ARM med dynamisk lenket glibc. Og ett enkelt bevis kan koste hundrevis av millioner tokener, som selskapet kaller et sentralt åpent problem.
Separat skrev Claude en spesifikasjon ut fra RFC 1950 og beviste at Linux-kjernens zlib-implementasjon oppfyller den på x86-binærnivå. Anthropic sier det gjentok dette for rundt seks andre mye brukte biblioteker. Om det x86-arbeidet lar seg generalisere videre, er det som bør følges.
