Claude beviste minnesikkerhet i 123 biblioteker – under strenge forutsetninger

Claude beviste minnesikkerhet i 123 biblioteker – under strenge forutsetninger

Anthropic publiserte 22. oktober 2026 resultater som selskapet selv beskriver som den første storskala, KI-drevne formelle verifiseringen av produksjonsprogramvare på maskinkodenivå. Rundt 180 millioner linjer med Rocq-bevis ble godkjent av bevissjekkeren – men garantiene gjelder kun under snevre antakelser, og flere av de mest konkrete tallene stammer foreløpig fra sekundærkilder som siterer utgivelsen.

Selskapets Frontier Red Team – i samarbeid med Theorem Labs, ifølge Crypto Briefing – fikk Claude til å produsere maskinsjekkede formelle bevis for at kompilerte programmer eksiterer normalt uten minnesikkerhetsfeil eller assertionsfeil, for alle inndata under 64 MB. Rundt 180 millioner linjer med bevis i bevisspråket Rocq ble godkjent av bevissjekkeren, spredt over 239 inngangspunkter i 123 åpne biblioteker fra OSS-Fuzz (Anthropic; ChainCatcher).

Tallene er slående, men de krever presis lesing. Bevisene gjelder under snevre antakelser: enkelttrådede, statiske binærfiler med fast minnebudsjett på en RISC-V-prosessor med Linux, hvor operativsystemets responser er modellert, ikke kjørt. Anthropic understreker selv at resultatet ikke betyr at bibliotekene er frie for sårbarheter.

Hva som faktisk er bevist

Kjernen i resultatet er en eksistensgaranti: Anthropic skriver at Claude beviste at de aktuelle programmene «alltid vil eksitere normalt uten å utløse minnesikkerhetsfeil eller mislykkede assertions, for ethvert inndata under 64 MB og enhver modellert Linux-respons og minnelayout» (Anthropic). Formuleringen «ethvert inndata under 64 MB» er det som skiller dette fra testing: en fuzz-test kan prøve millioner av inndata, et formelt bevis dekker i prinsippet alle samtidig.

Men garantien hviler på fire antakelser som bør leses nøye:

• RISC-V, ikke x86 eller ARM. Bevisene retter seg mot kompilerte RISC-V-instruksjoner (Anthropic; ChainCatcher). Det samme biblioteket kompilert for en annen arkitektur er ikke dekket.
• Enkelttrådede, statiske binærfiler. Konkurransetilstander mellom tråder, dynamisk linkede biblioteker og kompleks oppstartskonfigurasjon faller utenfor.
• Fast minnebudsjett. Programmet antas å operere med et fastlagt minnetak.
• Modellert Linux. Operativsystemets responser og minnelayout er modellert i bevisene. En modell er ikke selve kjernen – hvis modellen avviker fra den virkelige Linux-oppførselen, gjelder ikke beviset automatisk for den kjørende programvaren.

Innenfor disse rammene er bevisene maskinsjekkede: Rocq-kjernen har verifisert at hver slutning følger av de forrige, fra aksiomer ned til maskininstruksjoner. Det betyr at selve bevisene ikke kan inneholde logiske feil som sjekkeren har oversett. Det betyr ikke at spesifikasjonene – påstandene om hva som skulle bevises – stemmer med det brukeren faktisk ønsker. Anthropic peker selv på dette: bevissjekkeren kan ikke bekrefte at spesifikasjonene samsvarer med virkeligheten (gjengitt i ChainCatchers dekning av utgivelsen). Et bevis er bare så sterkt som spesifikasjonen det beviser.

Hvordan det ble gjort: fra fuzz-tester til formelle spesifikasjoner

Den tekniske inngangen var Google OSS-Fuzz, Googles tjeneste som kontinuerlig fuzz-tester åpen kildekode-biblioteker. OSS-Fuzz-prosjektene kommer med kompilbare fuzz-tester – små programmer som kaller bibliotekets inngangspunkter med genererte inndata. Teamet gjorde disse testene om til formelle spesifikasjoner: i stedet for å kjøre testen med utvalgte inndata, formulerte de testen som en matematisk påstand om alle mulige inndata (ChainCatcher).

Deretter fikk Claude i oppgave å bevise egenskapene på maskinkodenivå. Det er et vesentlig valg: bevis på kildekodenivå krever at man stoler på at kompilatoren gjør det den skal. Ved å rette bevisene mot de kompilerte RISC-V-instruksjonene eliminerer man det trinnet – garantien gjelder det som faktisk kjøres på prosessoren, ikke det som sto i C-koden.

Prosessen var ikke renvinnende fra første forsøk. ChainCatcher skriver at Claude beviste egenskapene for 239 inngangspunkter i 123 biblioteker «etter å ha patchet identifiserte problemer» – altså at arbeidet avdekket feil i selve bibliotekene som måtte fikses før bevisene kunne fullføres (ChainCatcher). Det hele skal ha skjedd «innen uker», ifølge samme kilde.

Skalaen i tall – og hva som hviler på sekundærkilder

Tallmaterialet kan deles i to lag: det som står i Anthropics publisering, og det som foreløpig er kjent gjennom dekning av utgivelsen og dens appendix.

Fra Anthropics egen publisering (Anthropic):

• 123 åpne kildekode-biblioteker.
• Inndatagrense på 64 MB.
• Antakelsene om enkelttrådet, statisk binærfil med fast minnebudsjett på RISC-V med Linux.
• seL4-sammenligningen: det tok to personår å implementere seL4-kjernen, men 20 personår å formelt verifisere den. Ifølge Anthropic er derfor formell verifisering praktisk bare i oppdragskritiske systemer, som luftfartskritisk kode hos Airbus.

Fra sekundærkilder som siterer utgivelsen og dens appendix (ChainCatcher; Unite.AI):

• 239 inngangspunkter i 123 biblioteker.
• Rundt 180 millioner linjer Rocq godkjent av bevissjekkeren.
• Rundt 1 milliard linjer Rocq skrevet totalt – altså at omtrent 18 % av modellens bevisforsøk overlevde sjekkeren.
• cJSON: et inngangspunkt i en parser på 391 linjer kode krevde et bevis på 630 000 linjer. fftw3, med 51 000 kodelinjer linket inn, krevde 480 000 bevislinjer.

Forholdstallet i cJSON er det mest illustrerende tallet i materialet: beviset var over 1600 ganger lengre enn koden det beviste. Det peker på hvorfor formell verifisering historisk har vært uoverkommelig for vanlig programvare – ikke fordi påstandene er vanskelige, men fordi arbeidsmengden i bevisføring er enorm. 180 millioner godkjente linjer er, med Anthropics seL4-tall som målstick, en oppgave som tradisjonelt ville målt i titalls personår.

Et viktig forbehold om kildelag: detaljene om 239 inngangspunkter, 180 millioner linjer, feilantallet og tolkprosjektet er her hentet fra ChainCatchers og Unite.AIs gjengivelse av utgivelsen, ikke verifisert direkte mot den fulle primærteksten. Dersom sekundærkildene har oppsummert riktig, er bildet som beskrevet.

Feilene som ble avdekket

Bevisføringen fungerte også som en uvanlig aggressiv feilsøker. Ifølge Unite.AI, som siterer appendix i utgivelsen, dukket det opp hundrevis av bugs underveis, inkludert en gjenoppdagelse av CVE-2026-56132 i libexpat (Unite.AI).

Det er verdt å merke seg hva slags funn dette er: ikke en ny oppdagelse fra grunnen av, men en uavhengig gjenoppdagelse av en allerede registrert sårbarhet – funnet ved matematisk resonnering over kompilert kode, ikke ved å kjøre programmet. Slik fungerer god formell verifisering som en feilsøker: den finner innganger som utløser udefinert oppførsel, uten at noen har kjørt dem.

Alvoret i disse feilene, inkludert underflow-feilen i dekompresjonskoden og feilen i PDF-leseren som nevnes i dekningen, hviler på Anthropics egen rapportering. Det foreligger ingen uavhengig sikkerhetsvurdering i kildematerialet, og denne artikkelen er heller ikke det. Behandling av CVE-2026-56132 bør derfor leses som «Anthropic rapporterer», ikke som et etablert faktum om alvorlighetsgrad.

Tilleggsresultater: zlib og en Python-tolk

Prosjektet omfattet to oppgaver utover minnesikkerhetsbevisene, kjent gjennom Unite.AIs dekning av utgivelsen (Unite.AI):

Formell spesifikasjon av RFC 1950. Anthropic ba Claude om å skrive en formell spesifikasjon av RFC 1950, dokumentet som definerer zlib-kompresjonsformatet, og deretter bevise at Linux-kjernens zlib-implementering oppfyller den – på x86-maskinkodenivå. Dette er en annen type garanti enn minnesikkerheten: ikke «programmet krasjer ikke», men «programmet gjør det spesifikasjonen sier». Slike funksjonelle korrekthetsbevis er historisk enda dyrere enn sikkerhetsbevis, og gjennomføringen på maskinkodenivå for en implementering i Linux-kjernen er i den forstand kanskje mer banebrytende enn selve hovedresultatet.

En Rust-implementert Python-tolk. Teamet bygde en Python-tolk i Rust og viste at den matcher CPython på 99,95 % av over 1,7 millioner tilfeldig genererte programmer. Merk forskjellen i karakter: dette er omfattende differensialtesting med tilfeldig genererte programmer, ikke formelle bevis. 99,95 % er imponerende, men 0,05 % av 1,7 millioner er rundt 850 avvik – og et avvik i en tolk kan være alt fra en kosmetisk forskjell til en sikkerhetsrelevant atferdsforskjell. Kilden angir ikke alvoret av avvikene.

Hva som fortsatt ikke er bevist

Anthropics egne forbehold er tydelige og bør gjentas like tydelig som resultatet:

1. Bibliotekene er ikke sårbarfrie. Selskapet skriver uttrykkelig at resultatet ikke betyr at bibliotekene er frie for sårbarheter – gjenværende problemer kan ligge utenfor de klarerte komponentene eller utenfor bevisenes omfang (ChainCatcher). «Klarerte komponenter» er nøkkelfrasen: formelle bevis hviler alltid på et fundament av aksiomer og antakelser som ikke selv er bevist. Kompilatoren, maskinmodellen, OS-modellen og spesifikasjonene er ikke en del av det som er verifisert her.
2. Spesifikasjon–virkelighet-gapet. Bevissjekkeren kan ikke bekrefte at spesifikasjonene stemmer med virkeligheten. Et bevis på at «programmet eksiterer normalt under disse antakelsene» er bare maksimalt verdifullt dersom antakelsene dekker hvordan programvaren faktisk kjøres i produksjon.
3. «Første gang»-påstanden er Anthropics egen. Selskapet karakteriserer dette som den første kjente storskala, KI-drevne formelle verifiseringen av produksjonsprogramvare på maskinkodenivå. Det er en påstand om pionerarbeid som ikke kan etterprøves uten en systematisk gjennomgang av tidligere arbeid i feltet, og som derfor kun kan tilskrives selskapet.
4. Partnerrollen er uklar. Crypto Briefing skriver at arbeidet kommer fra Frontier Red Team «i samarbeid med et firma kalt Theorem Labs» (Crypto Briefing); Unite.AI omtaler samarbeidet som «Theorem». Forfatterlisten skal ifølge Crypto Briefing inkludere sikkerhetsforskere som Keane Lucas, Chris Rohlf, Nicholas Carlini og Nickolai Zeldovich. Den nøyaktige rollefordelingen mellom selskapene er ikke uavhengig verifisert.

Hva det betyr: økonomien i verifisering

Den egentlige saken er ikke 123 biblioteker. Det er seL4-tallet: 20 personår verifisering mot to personår implementering er forholdet som ifølge Anthropic har holdt formell verifisering utelukket fra all programvare som ikke styrer oppdragskritiske systemer. Har Anthropic rett i at Claude kunne produsere tilsvarende sjekker-verifiserte bevis «innen uker», endres kostnadskurven for hele disiplinen – i hvert fall for programvare som kan kompileres til enkelttrådede statiske binærfiler på RISC-V.

Tre forhold demper konklusjonen foreløpig:

• Begrunnelsen hviler på selskapets egen evaluering. Dette er Anthropic som viser frem sin egen modells egenskaper, ikke en uavhengig replikasjon. Tallene i appendix er ikke etterkontrollert av tredjepart i kildematerialet.
• Antakelsene begrenser overførbarheten. Resultatet sier lite direkte om typiske produksjonsmiljøer: flertrådede programmer, dynamisk lastet kode, andre instruksjonssettmiljøer, eller interaksjoner med en ekte kjerne fremfor en modell.
• Gjenbrukbarheten er uavklart. Det er ukjent fra kildene hvor mye av metodikken som er prosjektspesifikk, og hvor mye som kan gjentas på nye biblioteker uten manuelt spesifikasjonsarbeid.

Hvis tallene holder under uavhengig etterkontroll, er det likevel en betydelig hendelse: bevis på minnesikkerhet på maskinkodenivå for hundrevis av inngangspunkter i mye brukt åpen kildekode, produsert autonomt av en språkmodell og sjekket av en bevissjekker. Det er den slags resultat som historisk har krevd akademiske flerårsprosjekter. Å vite nøyaktig hva som er bevist – og hva som ikke er – er forutsetningen for å vurdere om dette er et gjennombrudd i økonomien bak formell verifisering, eller en imponerende demonstrasjon med snevrere rekkevidde enn overskriftene antyder.