Anthropic sier at Claude beviste sikkerhetsegenskaper i 123 biblioteker

Anthropic publiserte forskning 22. oktober 2026 og rapporterte at Claude utarbeidet maskinkontrollerte formelle bevis for sikkerhetsegenskaper på RISC-V-assemblernivå for 239 inngangspunkter til fuzz-tester i 123 biblioteker med åpen kildekode, i samarbeid med Theorem.

Ifølge Anthropic rettet Claude feilene det fant, og beviste deretter at programmene alltid vil avsluttes normalt uten å utløse minnesikkerhetsfeil eller bryte assertions, for alle inndata under 64 MB og alle modellerte svar fra Linux-operativsystemet og minneoppsett. Bevisene forutsetter at programmet kjører som en statisk binærfil med én tråd og et fast minnebudsjett på en RISC-V-prosessor med Linux. Anthropic sa at bevisene består av rundt 180 millioner linjer Rocq, og at et typisk bevis er på rundt 600 000 linjer og dekker binærfiler med en medianlengde på 18 000 RISC-V-instruksjoner. Selskapet sa at dette, så vidt det vet, er det første storstilte forsøket på å bruke KI til å anvende formell verifikasjon på produksjonsprogramvare på assemblerspråknivå.

Et utvalg av bevisene, sammen med semantikken for RISC-V og operativsystemet som ligger til grunn for dem, publiseres på GitHub. Anthropic sa at selskapet også offentliggjør de tillitssikrede komponentene som ble utviklet for prosjektet og ikke allerede er offentlige, fullstendige bevis for fuzz-tester som ikke krevde feilrettinger, og spesifikasjoner for fuzz-tester det ikke klarte å bevise, samtidig som det holder tilbake bevis som kan avsløre en feil som ikke er rettet.

Fra fuzz-tester til formelle bevis

Metoden gjør hver av bibliotekenes eksisterende, kompilerbare fuzz-tester om til en formell spesifikasjon som uttrykker én regel: Testen krasjer aldri for inndata under 64 MB. Spesifikasjonen defineres over kompilerte RISC-V-instruksjoner ved hjelp av Theorems formelle semantikk for RISC-V-instruksjonssettet og Linux-prosesser, og Rocq-beviskontrolleren verifiserer hvert ferdig bevis mot spesifikasjonen. Anthropic sier at dette begrenser det utviklerne må stole på, til tre komponenter: de formelle modellene av RISC-V og Linux-prosesser, de nøyaktige teoremutsagnene og selve Rocq-kontrolleren.

Anthropic sa at selskapet brukte denne prosessen på hundrevis av prosjekter i Googles OSS-Fuzz-initiativ, som tilbyr kontinuerlig fuzz-testing for kvalifiserte prosjekter med åpen kildekode og automatisk instrumenterer C- og C++-programmer med AddressSanitizer, et verktøy som får et program til å krasje hver gang minnet brukes på feil måte. Et appendiks datert 22. oktober 2026 beskriver det fullstendige teoremet som ble bevist: For alle inndata under 64 MiB og alle minneoppsett får verken den AddressSanitizer-instrumenterte binærfilen eller den vanlige binærfilen en feil, avbrytes eller viser umodellert atferd, og begge produserer identiske lese- og skrivespor, avslutningsatferd og endelig filsystemtilstand.

Appendikset opplyser at Claude skrev rundt én milliard linjer Rocq i løpet av arbeidet, hvorav rundt 180 millioner linjer besto beviskontrollen. Inngangspunktet til cJSON-parseren, på 391 linjer, fikk et bevis på 630 000 linjer, mens fftw3, med 51 000 linjer lenket inn, fikk et bevis på 480 000 linjer. Fordi Claude fikk lov til å endre kode før et bevis var fullført, sa Anthropic at selskapet trakk poeng for feilrettinger, ga ekstra uttelling for å bevise hvilke inndata en feilretting endret, og loggførte og reviderte feilrettingene for å motvirke manipulering av belønningssystemet.

Feil oppdaget under forsøk på å bevise

Anthropic rapporterer at forsøkene på å bevise programmene avdekket hundrevis av feil, mange av dem feil som en fuzzer neppe ville ha funnet. Mens Claude beviste inngangspunktet til ett bibliotek, fant det en underflyt i en dekomprimerer som førte til en skriving utenfor grensene, men bare for inndata på rundt 20 MB med ett sjeldent og spesifikt oppsett. Andre funn omfattet en lesing utenfor grensene i en bildeavkoder som krevde 64 MB inndata og mer enn 2 GB minne, en lesing utenfor grensene som krevde en bestemt rekkefølge av kall på tvers av to håndtak til samme fil, og et gjenfunn av CVE-2026-56132 i libexpat, som krevde dypt nøstede inndata.

Claude fant også logiske feil som aldri fører til krasj, blant annet en begrensning på hvilke filer et program kan laste inn, som ikke alltid håndheves. Anthropic sa at verifiseringsforsøk på flere mye brukte, kritiske applikasjoner avdekket en tidligere ukjent logisk feil som hadde ligget latent i mer enn ti år, og at selskapet i løpet av et forsøk på å verifisere en mye brukt PDF-leser fant like mange sikkerhetsfeil på én uke som det vanligvis rapporteres om på et år.

Ytterligere eksperimenter og funn om effektivitet

I tillegg til OSS-Fuzz ba Anthropic Claude om å skrive en formell spesifikasjon av RFC 1950, det tekniske dokumentet som definerer zlib-komprimeringsformatet, og deretter bevise at Linux-kjernens zlib-implementering følger spesifikasjonen korrekt. Claude beviste den x86-kompilerte binærfilen direkte ved hjelp av formell semantikk for x86-instruksjonssettet som Claude hadde generert, og Anthropic sa at selskapet gjentok prosessen for et halvt dusin andre mye brukte biblioteker og fant mindre, ikke-utnyttbare feil i spesielle randtilfeller, som nå rapporteres til de oppstrøms vedlikeholderne. Selskapet rapporterte også at genereringen av x86-semantikken avdekket hundrevis av feil i den offisielle referansedokumentasjonen og et mindre antall feil i selve maskinvaren, og at trinnvis kjøring gjennom semantikken kan starte et Ubuntu-brukermiljø på en Linux-kjerne.

I et annet eksperiment bygde Claude en tolk for en stor delmengde av Python i Rust og beviste ved hjelp av verifikasjonsverktøyet Verus at den følger CPython-semantikken som er beskrevet i en akademisk artikkel. Det tekniske vedlegget oppgir at alle tolkens 17 nivåer ble bevist, med teoremet «Når tolken returnerer et resultat, er dette resultatet det den formelle semantikken foreskriver.» Anthropic sa at empirisk testing av 1,7 millioner tilfeldig genererte Python-programmer viste identisk oppførsel som CPython i 99,95 % av testene. Av sju feil som ble lagt inn med hensikt, overlevde fem tilfeldig testing, mens alle sju brøt beviset.

For å måle effektiviteten laget Anthropic 36 små verifikasjonsoppgaver ved å forenkle faktiske inngangspunkter fra OSS-Fuzz. Dette ga programmer på 283–2 491 instruksjoner, med inndata begrenset til 64 byte og AddressSanitizer erstattet av en «mini-ASan»-kjøretidskomponent på rundt 100 instruksjoner. Anthropic rapporterer at Opus 5.5 beviser halvparten av oppgavene med rundt 40 % færre tokener enn Opus 5. Anthropic rapporterer også at agenter som kunne kopiere hverandres bevis i et delt arbeidsområde, trengte 17 % færre tokener enn agenter som jobbet alene, at noen lyktes etter først å ha mislyktes alene, og at agenter som jobbet alene, ikke klarte å fullføre to av bevisene. Selskapet sa at den samme gjenbrukseffekten viste seg i stor skala under OSS-Fuzz-arbeidet, der agentteam kopierte ferdige bevis og tilpasset dem fordi mye av hvert bevis omfatter felles C-kjøretidskode og initialiseringskode for AddressSanitizer.

Oppgitte begrensninger og OSS Verify-programmet

Anthropic understreker at bevisene ikke betyr at bibliotekene er feilfrie: Gjenværende feil kan ligge i de betrodde komponentene eller utenfor bevisenes virkeområde. Bevisene gjelder entrådede, statisk lenkede RISC-V-binærfiler som er lenket mot musl libc, mens de fleste brukerne kjører disse bibliotekene på x86 eller ARM og lenker dynamisk mot glibc. AddressSanitizer oppdager dessuten ikke alle minnesikkerhetsfeil. Selskapet sa at det forventer at disse begrensningene blir håndterbare etter hvert som modellene forbedres.

Theorem tilbyr den samme verifikasjonsprosessen gratis til kvalifiserte åpen kildekode-prosjekter gjennom programmet OSS Verify. Prosjekter melder seg på ved å sende inn en pull request som legger til filene project.yaml, Dockerfile og build.sh i programmets repository. Theorem sier at selskapet vurderer prosjektene etter omtrent de samme kriteriene som OSS-Fuzz og prioriterer kritisk infrastruktur som er mye brukt. Ifølge Theorem får vedlikeholderne et Rocq-bevis, kontrollert av Rocq-kjernen, på at hvert fuzz-mål ikke krasjer ved noen inndata på opptil 64 MiB. Feil som oppdages under arbeidet med beviset, meldes konfidensielt til vedlikeholderne per e-post, uten noen frist for offentliggjøring, og det kan ta flere dager å produsere bevisene. Theorems veikart har som mål å verifisere hele Nix-økosystemet, inkludert kritisk infrastruktur som glibc, OpenSSL og cURL.