Claude genererte formelle bevis for minnesikkerhet i 123 åpen kildekode-biblioteker, ned til RISC-V-maskinkode

Claude genererte formelle bevis for minnesikkerhet i 123 åpen kildekode-biblioteker, ned til RISC-V-maskinkode

Anthropic publiserte 22. oktober 2026 forskning der Claude skal ha produsert maskinsjekkede formelle bevis for minnesikkerhet i 239 inngangspunkter fordelt på 123 åpen kildekode-biblioteker, ned til kompilert RISC-V-maskinkode. Metoden avdekket ifølge selskapet feil som hadde overlevd billioner av fuzz-testforsøk – men bevisene er betingede, og garantiene hviler på komponenter ingen har sjekket.

Hva som faktisk er gjort

Utgangspunktet var eksisterende fuzz-tester – tester som fôrer programvare med tilfeldige eller muterte inndata for å finne krasj. Anthropic lot Claude omsette disse testene til matematiske spesifikasjoner: setningen som skulle bevises, var at de 239 inngangspunktene ikke krasjer for noe inndata under 64 MiB (MSN).

Selve bevisarbeidet skjer ikke i kildekoden, men i de kompilerte binærfilene. Spesifikasjonen er definert over kompilerte RISC-V-instruksjoner, ved hjelp av formell semantikk for RISC-V-instruksjonssettet og Linux-prosesser levert av samarbeidspartneren Theorem (Unite.AI). Det betyr at verifiseringen omfatter det prosessoren faktisk kjører – inkludert hva kompilatoren har gjort med koden – og ikke bare det utvikleren skrev.

Hvert ferdig bevis sjekkes uavhengig av Rocq, bevishjelpemiddelet tidligere kjent som Coq. Bevisene skal i gjennomsnitt være på rundt 600 000 linjer hver, med totalt rundt 180 millioner linjer Rocq-kode (Glitchwire). Ifølge et vedlegg datert 22. oktober 2026, gjengitt av Unite.AI, skrev Claude rundt én milliard linjer underveis – av disse passerte omtrent 180 millioner sjekkeren. Skillet mellom skrevet og akseptert kode er verdt å merke seg: mesteparten av arbeidet var mislykkede forsøk, og tallene bør bekreftes mot rapports primærkilde, som ikke foreligger blant de tilgjengelige kildene.

Anthropic fremstiller selv innsatsen som det første store tiltaket for å anvende KI-drevet formell verifisering på produksjonsprogramvare i denne skalaen, og hevder at det som tradisjonelt krever år med ekspertarbeid, ble gjort på noen få uker (Glitchwire). Begge påstandene er selskapets egne, ikke uavhengig verifiserte.

Feilene ingen fuzz-test fant

Poenget med bevis er at de dekker alle inndata, ikke bare de testeren tilfeldigvis genererte. Ifølge MSNs dekning avslørte bevisforsøkene feil som hadde overlevd anslagsvis billioner av fuzz-forsøk:

• En teller som kunne «underslu» (underflow) og utløse skriving utenfor gyldig minneområde under dekompresjon – feilen krevde inndata på rundt 20 MB med en sjelden datasammenstilling.
• En feil i en bildedekoder som krevde 64 MB inndata og mer enn 2 GB minne for å manifestere seg.

I tillegg gjenoppdaget Claude ifølge Unite.AI CVE-2026-56132 i libexpat, en sårbarhet som krever dypt nøstede inndata. Disse funnene hviler på Anthropics egen rapportering og er ikke uavhengig bekreftet.

Da modellen får lov å lappe koden

En metodologisk detalj fortjener oppmerksomhet: Claude fikk lov til å patche koden før et bevis ble fullført. Det åpner for en klassisk fallgruve i maskinlæring – «reward hacking», der modellen finter ut målet i stedet for å løse oppgaven, for eksempel ved å endre koden til noe trivielt som er lett å bevise.

Anthropic sier at selskapet motvirket dette på tre måter: patcher ble straffet i poengberegningen, modellen fikk tilleggscredit for å bevise hvilke inndata en patch endret virkningen av, og alle patcher ble loggført og revidert (Unite.AI). Det er fornuftige tiltak, men de er også selvvurderte – kvaliteten på revisjonen kan ikke etterprøves før materialet er offentliggjort.

Hvor garantiene stopper

Det viktigste forbeholdet står i Anthropics egen begrensningseksjon, gjengitt av Blockchain.News: bevisene er betingede og betyr ikke at programvaren er feilfri (Blockchain.News). Garantiene gjelder spesifikt:

• Enkelttrådede, statiske binærfiler med fast minnebudsjett på RISC-V Linux. Ekte produksjonsbruk med tråder, dynamisk lastning og andre plattformer dekkes ikke av modellen.
• Et begrenset sett med inngangspunkter. Arbeidet dekker ikke alle inngangspunkter eller alle måter programvaren brukes på i produksjon.
• Betingelser i spesifikasjonen. Beviset sier «ingen krasj for inndata under 64 MiB» – ikke fravær av alle typer sikkerhetsfeil.

I tillegg kommer det som i formell verifisering kalles den «tiltrodde basen»: semantikken for RISC-V og Linux, selve teoremformuleringene og Rocq-sjekkeren er komponenter som ikke er bevist. Dersom semantikken avviker fra hvordan en fysisk prosessor oppfører seg, overføres ikke garantien til virkeligheten. Usikkerheten er altså ikke borte, men konsentrert på færre, inspiserbare steder – forutsatt at noen faktisk inspiserer dem.

Hva som offentliggjøres – og hva som holdes tilbake

Anthropic oppgir at selskapet slipper et utvalg av bevisene, RISC-V- og OS-semantikken, de tiltrodde komponentene som ikke allerede er offentlige, fullstendige bevis for fuzz-tester som ikke krevde patching, og spesifikasjoner for tester det ikke lot seg bevise (Unite.AI). Bevis som kunne avsløre upatchede feil, holdes tilbake – et forståelig ansvarshensyn, men det betyr at det offentlige materialet ikke gir full innsikt i funnene.

Samarbeidet var mellom Anthropics Frontier Red Team og Theorem Labs, et oppstartsselskap i San Francisco grunnlagt i 2025 av Jason Gross og Rajashree Agrawal, ifølge Glitchwire. Andre kilder omtaler partneren bare som «Theorem», og navnet og selskapsopplysningene støttes kun av én kilde. Glitchwire oppgir videre – som eneste kilde – at Mozilla har kreditert Frontier Red Team med mer enn et dusin feil i Firefox før versjon 148.

Åpne spørsmål

Det tyngste forbeholdet er at ingen av de tilgjengelige kildene er Anthropics primære rapport. Alle sentrale tall – 180 millioner aksepterte linjer, én milliard skrevne, 239 inngangspunkter, 123 biblioteker, 64 MiB-grensen – stammer fra selskapet, formidlet gjennom sekundær dekning, og uavhengig verifisering foreligger ikke. Det gjelder også feilfunnene, inkludert gjenoppdagelsen av CVE-2026-56132 i libexpat.

Tre spørsmål vil avgjøre resultatets betydning. For det første: vil uavhengige sikkerhetsforskere godta den tiltrodde basen – særlig om RISC-V/Linux-semantikken faktisk matcher virkelige systemer? For det andre: er linjetallene og feilfunnene nøyaktige når primærrapporten kan etterprøves? For det tredje: er det repeterbart – kan andre gjøre det samme på annen programvare, eller krevde det Anthropics spesifikke modell og interne infrastruktur?

Det som likevel skiller dette fra de fleste «KI fant feil»-historier, er formatet. Et fuzz-funn er ett datapunkt; et maskinsjekket bevis er en garanti som gjelder alle inndata innenfor spesifikasjonen – på vilkår av det modellen og den tiltrodde basen faktisk beskriver. Hva som helst av hypen bør måles mot det Anthropic selv skriver i begrensningene: betingede garantier, ikke feilfri kode.