Anthropic siger, at Claude har bevist sikkerhedsegenskaber i 123 biblioteker

Anthropic publicerede forskning den 22. oktober 2026, hvor virksomheden rapporterede, at Claude i samarbejde med Theorem havde udarbejdet maskinkontrollerede formelle beviser for sikkerhedsegenskaber på RISC-V-assemblerkodeniveau for 239 indgangspunkter til fuzztest i 123 open source-biblioteker.

Ifølge Anthropic rettede Claude de fejl, som modellen fandt, og beviste derefter, at programmerne altid afsluttes normalt uden at udløse hukommelsessikkerhedsfejl eller få assertions til at fejle, uanset input under 64 MB og alle modellerede svar fra Linux-operativsystemet og hukommelseslayout. Beviserne forudsætter, at programmet kører som en enkelttrådet statisk binærfil med et fast hukommelsesbudget på en RISC-V-CPU med Linux. Anthropic sagde, at beviserne omfatter omkring 180 millioner linjer Rocq-kode, og at et typisk bevis fylder omkring 600.000 linjer og dækker binærfiler med en medianlængde på 18.000 RISC-V-instruktioner. Virksomheden sagde, at dette så vidt den ved er det første storstilede forsøg på at bruge AI til at anvende formel verifikation på produktionssoftware på assemblerkodeniveau.

Et udvalg af beviserne samt den RISC-V- og operativsystemsemantik, de bygger på, offentliggøres på GitHub. Anthropic sagde, at virksomheden også offentliggør de betroede komponenter, der blev udviklet til projektet, og som ikke allerede er offentligt tilgængelige, fuldstændige beviser for fuzztest, der ikke krævede rettelser, samt specifikationer for fuzztest, som det ikke lykkedes at bevise, mens beviser, der kunne afsløre en ikke-rettet fejl, tilbageholdes.

Fra fuzztest til formelle beviser

Metoden omdanner hver biblioteks eksisterende, kompilerbare fuzztest til en formel specifikation, der udtrykker én regel: Testen går aldrig ned for noget input under 64 MB. Specifikationen defineres ud fra kompilerede RISC-V-instruktioner ved hjælp af Theorems formelle semantik for RISC-V-instruktionssættet og Linux-processer, og Rocq-beviskontrollen verificerer hvert færdigt bevis i forhold til specifikationen. Anthropic siger, at det betyder, at udviklere kun behøver at have tillid til tre komponenter: de formelle modeller af RISC-V og Linux-processer, de præcise teoremsætninger og selve Rocq-kontrollen.

Anthropic sagde, at virksomheden anvendte denne proces på hundredvis af projekter i Googles OSS-Fuzz-initiativ, der leverer kontinuerlig fuzztest af kvalificerede open source-projekter og automatisk instrumenterer C- og C++-programmer med AddressSanitizer, et værktøj, der får et program til at gå ned, hver gang der foretages en ugyldig hukommelsesadgang. Et appendiks dateret 22. oktober 2026 beskriver det fulde teorem, der blev bevist: For alle input under 64 MiB og alle hukommelseslayout giver hverken den AddressSanitizer-instrumenterede binærfil eller den almindelige binærfil fejl, afbrydes eller udviser ikke-modelleret adfærd, og begge producerer identiske læse- og skrivespor, afslutningsadfærd og endelig filsystemtilstand.

Appendikset oplyser, at Claude skrev omkring én milliard linjer Rocq-kode under arbejdet, hvoraf omkring 180 millioner linjer bestod beviskontrollen. cJSON’s parserindgangspunkt på 391 linjer fik et bevis på 630.000 linjer, mens fftw3, med 51.000 linjer linket ind, fik et bevis på 480.000 linjer. Da Claude havde tilladelse til at rette kode, før et bevis blev færdiggjort, sagde Anthropic, at virksomheden straffede rettelser, gav ekstra belønning for at bevise, hvilke input en rettelse ændrede, og førte log over og reviderede rettelserne for at modvirke manipulation af belønningssystemet.

Fejl fundet under forsøg på at bevise egenskaber

Anthropic rapporterer, at forsøgene på at føre beviserne igennem afslørede hundredvis af fejl, hvoraf mange næppe ville være blevet fundet af en fuzztester. Mens Claude forsøgte at bevise et biblioteks indgangspunkt, fandt modellen et tællerunderløb i en dekomprimeringsfunktion, som medførte en skrivning uden for gyldigt område, men kun ved input på omkring 20 MB med ét sjældent, specifikt layout. Andre fund omfattede en læsning uden for gyldigt område i en billeddekoder, der krævede et input på 64 MB og mere end 2 GB hukommelse, en læsning uden for gyldigt område, der krævede en bestemt rækkefølge af kald på tværs af to håndtag til den samme fil, samt genopdagelsen af CVE-2026-56132 i libexpat, som krævede dybt indlejret input.

Claude fandt også logikfejl, der aldrig får programmet til at gå ned, herunder en begrænsning på, hvilke filer et program kan indlæse, som ikke altid håndhæves. Anthropic sagde, at forsøg på at verificere flere udbredte, kritiske programmer afslørede en hidtil ukendt logikfejl, der havde ligget latent i mere end et årti, og at virksomheden under et forsøg på at verificere en udbredt PDF-læser fandt lige så mange sikkerhedsfejl på én uge, som der typisk indrapporteres på et år.

Yderligere eksperimenter og effektivitetsresultater

Ud over OSS-Fuzz bad Anthropic Claude om at skrive en formel specifikation af RFC 1950, det tekniske dokument, der definerer zlib-komprimeringsformatet, og derefter bevise, at Linux-kernens zlib-implementering implementerer det korrekt. Claude beviste direkte den x86-kompilerede binærfil ved hjælp af formel semantik for x86-instruktionssættet, som Claude selv havde genereret, og Anthropic sagde, at virksomheden gentog processen for et halvt dusin andre udbredte biblioteker og fandt mindre, ikke-udnyttelige randtilfældefejl, som indrapporteres til de respektive upstream-projekter. Virksomheden rapporterede også, at genereringen af x86-semantikken afslørede hundredvis af fejl i den officielle refer dokumentation og et mindre antal fejl i selve hardwaren, og at trinvis eksekvering af semantikken kan starte et Ubuntu-brugermiljø på en Linux-kerne.

I et andet eksperiment byggede Claude en fortolker til en stor delmængde af Python i Rust og beviste ved hjælp af verificeringsværktøjet Verus, at den følger CPython-semantikken, som er beskrevet i en akademisk artikel. Det tekniske appendiks fastslår, at alle fortolkerens 17 niveauer blev bevist, og at sætningen holder: “Når fortolkeren returnerer et resultat, er resultatet det, som den formelle semantik foreskriver.” Anthropic oplyste, at empiriske test af 1,7 millioner tilfældigt genererede Python-programmer viste identisk adfærd med CPython i 99,95 % af testene; af syv fejl, der bevidst blev indført, overlevede fem tilfældige test, mens alle syv brød beviset.

For at måle effektiviteten byggede Anthropic 36 små verificeringsopgaver ved at gøre reelle OSS-Fuzz-indgangspunkter mindre, så der blev produceret programmer på 283–2.491 instruktioner med input begrænset til 64 bytes og AddressSanitizer erstattet af en “mini-ASan”-runtime på omkring 100 instruktioner. Anthropic rapporterer, at Opus 5.5 beviser halvdelen af opgaverne med omkring 40 % færre tokens end Opus 5. Anthropic rapporterer også, at agenter, som måtte kopiere hinandens beviser i et fælles arbejdsområde, havde brug for 17 % færre tokens end agenter, der arbejdede alene; nogle lykkedes efter tidligere at være mislykkedes på egen hånd, og agenter, der arbejdede alene, kunne ikke færdiggøre to af beviserne. Virksomheden sagde, at den samme genbrugseffekt viste sig i stor skala under OSS-Fuzz-indsatsen, hvor agenthold kopierede færdige beviser og tilpassede dem, fordi en stor del af hvert bevis omfatter fælles initialiseringskode for C-runtime og AddressSanitizer.

Oplyste begrænsninger og OSS Verify-programmet

Anthropic understreger, at beviserne ikke betyder, at bibliotekerne er fejlfri: Resterende fejl kan befinde sig i de betroede komponenter eller ligge uden for bevisernes omfang. Beviserne dækker enkelttrådede, statiske RISC-V-binærfiler, der er linket mod musl libc, mens de fleste brugere kører bibliotekerne på x86 eller ARM og linker dynamisk mod glibc, og AddressSanitizer opdager ikke alle fejl vedrørende hukommelsessikkerhed. Virksomheden sagde, at den forventer, at disse begrænsninger bliver håndterbare, efterhånden som modellerne forbedres.

Theorem tilbyder den samme pipeline gratis til open source-projekter, der opfylder kravene, gennem programmet OSS Verify. Man tilmelder sig ved at sende en pull request, der tilføjer filerne project.yaml, Dockerfile og build.sh til programmets repository, og Theorem siger, at virksomheden gennemgår projekterne efter retningslinjer, der ligner OSS-Fuzz’, med prioritet til kritisk infrastruktur, der bruges bredt. Ifølge Theorem modtager vedligeholderne et Rocq-bevis, som kontrolleres af Rocq-kernen, for, at hvert fuzzmål ikke går ned ved noget input på op til 64 MiB; fejl, der findes under bevisarbejdet, meddeles vedligeholderne fortroligt via e-mail uden nogen frist for offentliggørelse, og det kan tage flere dage at udarbejde beviserne. Theorems køreplan sigter mod at verificere hele Nix-økosystemet, herunder kritisk infrastruktur som glibc, OpenSSL og cURL.