Anthropic och Theorem rapporterar maskinkontrollerbara säkerhetsbevis för 239 ingångspunkter i 123 öppna kodbibliotek. Resultatet gäller specificerade egenskaper hos kompilerade program under bestämda antaganden. Det betyder inte att alla bibliotekens funktioner är buggfria.
Forskningen publicerades den 22 oktober 2026. Claude hjälpte till att skriva bevis som kontrolleras med ett separat bevissystem. För utvecklare är den viktiga frågan därför både vad beviset säger och vilka delar av den verkliga miljön det omfattar.
Testning och bevis svarar på olika frågor
Tänk dig en funktion som läser en datafil. Ett test kan ge den en viss trasig fil och kontrollera att den inte kraschar. Fuzzing varierar indata för att försöka hitta fler fel. Ett formellt bevis kan i stället gälla alla indata inom en uttryckligt beskriven gräns, men bara för den egenskap och maskinmodell som definierats.
Detta är ett pedagogiskt exempel. Tekniksvar har inte genomfört ett sådant test eller producerat ett bevis.
Vilka gränser gäller forskningen?
Anthropic beskriver statiskt länkade, enkeltrådade RISC-V-binärer och bevis om bland annat uteblivna krascher för indata under 64 MB vid undersökta fuzz-ingångar. Vanlig drift på x86 eller ARM med dynamiskt länkade bibliotek omfattas inte automatiskt.
Forskarna verifierade inte varje ingångspunkt eller allt beteende i varje bibliotek. Beviskontrollanten kan dessutom kontrollera att beviset följer specifikationen utan att avgöra om specifikationen beskriver hela den verkliga datorn korrekt.
| Fråga | Vad behöver granskas? |
|---|---|
| Vad är bevisat? | Den precisa satsen och indataförutsättningarna |
| För vilket program? | Den kompilerade binären och dess byggkedja |
| På vilken maskinmodell? | Antaganden om processor, operativsystem och minne |
| Gäller vår produkt samma sak? | Skillnader i version, anrop, plattform och integration |
Den offentliga delmängden är mindre
Vid kontroll den 25 oktober anger Theorems offentliga repository 60 ingångspunkter i 25 bibliotek, med bevis som kontrolleras i Rocq 9.2.0. Det är en publicerad delmängd, inte samma omfattning som forskningsrapportens 239/123.
README beskriver modellen LPS, en formell Linux-processmodell som kör RISC-V-binärer. Projektet pekar uttryckligen på antaganden som modellen inte kontrollerar. Ett lyckat bevis är därmed också beroende av det som lagts in i den betrodda modellen.
Den verkliga skärmbilden ovan visar repositoryts README. Dokumentationen är MIT-licensierad; licenstext och projektets NOTICE följer med bilden. Vi har inte kört eller reproducerat bevisen.
Vad bör en kodansvarig göra med resultatet?
Använd ett verifieringspåstående som en preciserad uppgift att granska. Be om version, byggförutsättningar, sats och återstående antaganden. Jämför sedan dessa med miljön där biblioteket faktiskt används.
Behåll tester, fuzzing, kodgranskning och säkerhetsuppdateringar. Ett bevis om en viss inläsningsväg avgör inte om applikationen runt biblioteket hanterar behörigheter rätt eller om en annan funktion innehåller fel.
Forskarnas uppgifter om buggar som hittades under arbetet visar också att beviskonstruktion kan hjälpa till att precisera problem. Påståenden om framtida bred användning är däremot deras bedömning, inte ett installationslöfte för den vanliga Claude-appen.
Källorna kontrollerades den 25 oktober 2026.
