Anthropic säger att Claude bevisat säkerhetsegenskaper i 123 bibliotek

Anthropic publicerade forskning den 22 oktober 2026 och rapporterade att Claude tog fram maskinkontrollerade formella bevis för säkerhetsegenskaper på RISC-V-assemblerkodnivå för 239 ingångspunkter i fuzzningstester i 123 bibliotek med öppen källkod, i samarbete med Theorem.

Enligt Anthropic åtgärdade Claude de buggar som upptäcktes och bevisade sedan att programmen alltid avslutas normalt utan att utlösa minnessäkerhetsfel eller fallera på assert-satser, för alla indata under 64 MB och alla modellerade svar från Linux-operativsystemet och minneslayouter. Bevisen förutsätter att programmet körs som en entrådad statisk binär med en fast minnesbudget på en RISC-V-processor med Linux. Anthropic uppgav att bevisen omfattar omkring 180 miljoner rader Rocq, och att ett typiskt bevis omfattar cirka 600 000 rader för att täcka binärer med en medianlängd på 18 000 RISC-V-instruktioner. Företaget uppgav att detta, såvitt det känner till, är det första storskaliga försöket att använda AI för att tillämpa formell verifiering på produktionsprogramvara på assemblerkodnivå.

Ett urval av bevisen, tillsammans med den RISC-V- och operativsystemsemantik som ligger till grund för dem, publiceras på GitHub. Anthropic uppgav att företaget också släpper de betrodda komponenter som tagits fram för projektet och som inte redan är offentliga, fullständiga bevis för fuzzningstester som inte krävde några kodändringar samt specifikationer för fuzzningstester som det inte kunde bevisa, samtidigt som det undanhåller bevis som skulle kunna avslöja en bugg som inte åtgärdats.

Från fuzzningstester till formella bevis

Metoden omvandlar varje biblioteks befintliga kompilerbara fuzzningstest till en formell specifikation som uttrycker en regel: testet kraschar aldrig för några indata under 64 MB. Specifikationen definieras utifrån kompilerade RISC-V-instruktioner med hjälp av Theorems formella semantik för RISC-V-instruktionsuppsättningen och Linux-processer, och Rocq-beviskontrollen verifierar varje färdigt bevis mot specifikationen. Anthropic säger att detta innebär att utvecklare bara behöver lita på tre komponenter: de formella modellerna av RISC-V och Linux-processer, de exakta teoremsatserna och själva Rocq-kontrollen.

Anthropic uppgav att företaget tillämpade processen på hundratals projekt i Googles OSS-Fuzz-initiativ, som tillhandahåller kontinuerlig fuzzningstestning för kvalificerade projekt med öppen källkod och automatiskt instrumenterar C- och C++-program med AddressSanitizer, ett verktyg som får ett program att krascha när minnet används på ett otillåtet sätt. En bilaga daterad den 22 oktober 2026 redogör för hela teoremet som bevisats: för alla indata under 64 MiB och alla minneslayouter får varken den ASan-instrumenterade binären eller den vanliga binären fel, avbryts eller uppvisar omodellerat beteende, och båda ger identiska läs- och skrivspår, avslutsbeteenden och slutliga filsystemstillstånd.

I bilagan står det att Claude skrev omkring en miljard rader Rocq under arbetet, varav cirka 180 miljoner rader godkändes av beviskontrollen. Parserns ingångspunkt på 391 rader i cJSON fick ett bevis på 630 000 rader, medan fftw3, med 51 000 länkade rader, fick ett bevis på 480 000 rader. Eftersom Claude fick ändra kod innan ett bevis slutfördes uppgav Anthropic att företaget bestraffade kodändringar, gav extra poäng för att bevisa vilka indata en ändring påverkade samt loggade och granskade ändringarna för att motverka belöningsmanipulation.

Buggar som upptäcktes under bevisförsöken

Anthropic rapporterar att försöken att ta fram bevis avslöjade hundratals buggar, många av dem sådana som en fuzzer sannolikt inte skulle hitta. När Claude bevisade en ingångspunkt i ett bibliotek upptäckte det ett räknarunderflöde i ett dekomprimeringsprogram som ledde till en skrivning utanför minnesgränserna, men bara vid indata på omkring 20 MB med en sällsynt, specifik layout. Bland andra fynd fanns en läsning utanför minnesgränserna i en bildavkodare som krävde 64 MB indata och mer än 2 GB minne, en läsning utanför minnesgränserna som krävde en viss sekvens av anrop via två handtag till samma fil samt ett återupptäckande av CVE-2026-56132 i libexpat, som krävde djupt nästlade indata.

Claude hittade också logikbuggar som aldrig leder till en krasch, bland annat en begränsning av vilka filer ett program kan läsa in som inte alltid upprätthålls. Anthropic uppgav att verifieringsförsök med flera kritiska program som används i stor utsträckning avslöjade en tidigare okänd logikbugg som hade legat oupptäckt i mer än ett decennium, och att företaget under ett försök att verifiera en vanligt förekommande PDF-läsare hittade lika många säkerhetsbuggar på en vecka som vanligtvis rapporteras under ett helt år.

Ytterligare experiment och effektivitetsresultat

Utöver OSS-Fuzz bad Anthropic Claude att skriva en formell specifikation av RFC 1950, det tekniska dokument som definierar zlib-komprimeringsformatet, och därefter bevisa att Linuxkärnans zlib-implementation följer specifikationen korrekt. Claude bevisade den x86-kompilerade binären direkt med hjälp av formell semantik för x86-instruktionsuppsättningen som Claude själv genererat. Anthropic uppgav att företaget upprepade processen för ett halvdussin andra bibliotek som används i stor utsträckning och hittade mindre, icke-exploaterbara gränsfallsbuggar som nu rapporteras till respektive uppströmsprojekt. Företaget rapporterade också att genereringen av x86-semantiken identifierade hundratals fel i officiell referensdokumentation och ett mindre antal buggar i själva hårdvaran, samt att stegvis exekvering genom semantiken kan starta en Ubuntu-användarmiljö på en Linuxkärna.

I ett annat experiment byggde Claude en tolk för en stor delmängd av Python i Rust och bevisade med verifieringsverktyget Verus att den följer den CPython-semantik som beskrivs i en akademisk artikel. I det tekniska tillägget står det att alla 17 nivåer i tolken bevisades, och att satsen ”När tolken returnerar ett resultat är det resultat som den formella semantiken föreskriver.” Anthropic uppgav att empiriska tester av 1,7 miljoner slumpmässigt genererade Python-program visade identiskt beteende med CPython i 99,95 % av testerna. Av sju avsiktligt införda buggar upptäcktes fem inte vid slumpmässiga tester, medan alla sju gjorde att beviset inte höll.

För att mäta effektiviteten skapade Anthropic 36 mindre verifieringsuppgifter genom att krympa verkliga ingångspunkter för OSS-Fuzz. Det resulterade i program på 283–2 491 instruktioner, med indata begränsade till 64 byte och AddressSanitizer ersatt av en ”mini-ASan”-körmiljö på omkring 100 instruktioner. Anthropic uppger att Opus 5.5 bevisar hälften av uppgifterna med omkring 40 % färre token än Opus 5. Anthropic uppger också att agenter som fick kopiera varandras bevis i en gemensam arbetsyta behövde 17 % färre token än agenter som arbetade ensamma, att vissa lyckades efter att tidigare ha misslyckats på egen hand och att agenter som arbetade ensamma inte lyckades färdigställa två av bevisen. Företaget sade att samma återanvändningseffekt märktes i större skala under arbetet med OSS-Fuzz, där agentteam kopierade färdiga bevis och anpassade dem, eftersom en stor del av varje bevis omfattar gemensam C-körmiljö och initialiseringskod för AddressSanitizer.

Angivna begränsningar och OSS Verify-programmet

Anthropic påpekar att bevisen inte innebär att biblioteken är fria från buggar: kvarvarande buggar kan finnas i de betrodda komponenterna eller utanför bevisens omfattning. Bevisen gäller enkeltrådade, statiskt länkade RISC-V-binärer som är länkade mot musl libc, medan de flesta användare kör biblioteken på x86 eller ARM och länkar dem dynamiskt mot glibc. AddressSanitizer upptäcker inte heller alla minnessäkerhetsbuggar. Företaget sade att det förväntar sig att dessa begränsningar blir hanterbara i takt med att modellerna förbättras.

Theorem erbjuder samma verktygskedja kostnadsfritt till kvalificerade open source-projekt genom sitt program OSS Verify. Projekten ansluts genom en pull request som lägger till filerna project.yaml, Dockerfile och build.sh i programmets kodförråd. Theorem säger att företaget granskar projekten enligt principer som liknar OSS-Fuzz och prioriterar kritisk infrastruktur som används i stor utsträckning. Enligt Theorem får de ansvariga för projekten ett Rocq-bevis, kontrollerat av Rocq-kärnan, som visar att varje fuzzmål inte kraschar på någon indata på upp till 64 MiB. Buggar som upptäcks under arbetet med beviset meddelas projektens ansvariga privat via e-post, utan någon tidsfrist för offentliggörande, och det kan ta flera dagar att ta fram bevisen. Theorems färdplan siktar på att verifiera hela Nix-ekosystemet, inklusive kritisk infrastruktur som glibc, OpenSSL och cURL.