Anthropic zegt dat Claude de beveiligingseigenschappen van 123 bibliotheken heeft bewezen

Anthropic publiceerde onderzoek op 22 oktober 2026, waarin werd gemeld dat Claude machinaal gecontroleerde formele bewijzen heeft geleverd voor beveiligingseigenschappen op het niveau van RISC-V-assemblercode, voor 239 ingangspunten van fuzztests in 123 opensourcebibliotheken, in samenwerking met Theorem.

Volgens Anthropic heeft Claude de bugs die het vond verholpen en vervolgens bewezen dat de programma’s altijd normaal worden beëindigd, zonder geheugenveiligheidsfouten te veroorzaken of assertions te laten mislukken, voor elke invoer kleiner dan 64 MB en elke gemodelleerde reactie van het Linux-besturingssysteem en elke geheugenindeling. De bewijzen gaan ervan uit dat het programma als een statische binary met één thread en een vast geheugenbudget draait op een RISC-V-CPU met Linux. Anthropic zei dat de bewijzen ongeveer 180 miljoen regels Rocq omvatten en dat een doorsnee bewijs ongeveer 600.000 regels beslaat, voor binaries met een mediane lengte van 18.000 RISC-V-instructies. Voor zover het bedrijf weet, is dit de eerste grootschalige poging om AI te gebruiken voor formele verificatie van productiesoftware op het niveau van assemblercode.

Een deel van de bewijzen, samen met de RISC-V- en besturingssysteemsemantiek waarop ze zijn gebaseerd, wordt gepubliceerd op GitHub. Anthropic zei ook de voor het project ontwikkelde vertrouwde componenten uit te brengen die nog niet openbaar zijn, evenals volledige bewijzen voor fuzztests waarvoor geen aanpassingen nodig waren en specificaties voor fuzztests die niet konden worden bewezen. Bewijzen die een niet-verholpen bug aan het licht zouden kunnen brengen, worden niet vrijgegeven.

Fuzztests omzetten in formele bewijzen

Deze aanpak zet de bestaande compileerbare fuzztest van elke bibliotheek om in een formele specificatie die één regel vastlegt: de test crasht nooit bij invoer kleiner dan 64 MB. De specificatie is gedefinieerd aan de hand van gecompileerde RISC-V-instructies, met gebruik van Theorems formele semantiek voor de RISC-V-instructieset en Linux-processen. De Rocq-bewijschecker controleert elk voltooid bewijs aan de hand van de specificatie. Volgens Anthropic blijven hierdoor slechts drie componenten over die ontwikkelaars moeten vertrouwen: de formele modellen van RISC-V en Linux-processen, de exacte theoremaformuleringen en de Rocq-checker zelf.

Anthropic zei dit proces te hebben toegepast op honderden projecten binnen Googles OSS-Fuzz-initiatief. Dat initiatief biedt doorlopende fuzztests voor in aanmerking komende opensourceprojecten en voorziet C- en C++-programma’s automatisch van instrumentatie met AddressSanitizer, een hulpmiddel dat een programma laat crashen zodra geheugen onjuist wordt benaderd. Een appendix van 22 oktober 2026 beschrijft het volledige bewezen theorema: voor alle invoer kleiner dan 64 MiB en alle geheugenindelingen veroorzaken noch de met ASan geïnstrumenteerde binary, noch de gewone binary een fout of afbreking, en vertonen ze geen ongemodelleerd gedrag; bovendien produceren beide identieke lees- en schrijfsporen, beëindigingsgedrag en uiteindelijke bestandssysteemstatus.

In de appendix staat dat Claude tijdens het project ongeveer één miljard regels Rocq schreef, waarvan ongeveer 180 miljoen regels de bewijschecker doorstonden. Het parseringangspunt van cJSON, met 391 regels, kreeg een bewijs van 630.000 regels; fftw3, met 51.000 gekoppelde regels, kreeg een bewijs van 480.000 regels. Omdat Claude de code mocht aanpassen voordat het een bewijs afrondde, zei Anthropic dat het aanpassingen bestrafte, extra waardering toekende voor het bewijzen welke invoer door een aanpassing veranderde en de aanpassingen registreerde en controleerde om manipulatie van de beloning tegen te gaan.

Bugs ontdekt tijdens pogingen om bewijzen te leveren

Anthropic meldt dat de pogingen om de bewijzen te leveren honderden bugs aan het licht brachten, waarvan een fuzzer er veel waarschijnlijk niet zou vinden. Tijdens het bewijzen van het ingangspunt van een bibliotheek ontdekte Claude een onderloop van een teller in een decompressor, die leidde tot een schrijfactie buiten de grenzen, maar alleen bij invoer van ongeveer 20 MB met één zeldzame, specifieke geheugenindeling. Andere ontdekkingen waren onder meer een leesactie buiten de grenzen in een beelddecoder waarvoor een invoer van 64 MB en meer dan 2 GB geheugen nodig was, een leesactie buiten de grenzen die een bepaalde reeks aanroepen via twee handles naar hetzelfde bestand vereiste, en de herontdekking van CVE-2026-56132 in libexpat, waarvoor diep geneste invoer nodig was.

Claude ontdekte ook logische bugs die nooit tot een crash leiden, waaronder een beperking op welke bestanden een toepassing kan laden die niet altijd wordt afgedwongen. Anthropic zei dat verificatiepogingen bij verschillende veelgebruikte, kritieke toepassingen een niet eerder bekende logische bug aan het licht brachten die al meer dan tien jaar latent aanwezig was. Ook ontdekte het bedrijf tijdens een poging om een veelgebruikte pdf-lezer te verifiëren in één week evenveel beveiligingsbugs als er doorgaans in een jaar worden gemeld.

Aanvullende experimenten en bevindingen over efficiëntie

Naast OSS-Fuzz vroeg Anthropic Claude om een formele specificatie te schrijven van RFC 1950, het technische document waarin het zlib-compressieformaat wordt gedefinieerd, en vervolgens te bewijzen dat de zlib-implementatie van de Linux-kernel dit correct implementeert. Claude bewees rechtstreeks de voor x86 gecompileerde binary, met gebruik van door Claude gegenereerde formele semantiek van de x86-instructieset. Anthropic zei dat het dit proces herhaalde voor een half dozijn andere veelgebruikte bibliotheken en daarbij kleine, niet-uitbuitbare bugs in uitzonderlijke gevallen aantrof, die bij de upstreamprojecten worden gemeld. Het bedrijf meldde ook dat het genereren van de x86-semantiek honderden fouten in de officiële referentiedocumentatie en een kleiner aantal bugs in de hardware zelf aan het licht bracht, en dat het stap voor stap doorlopen van de semantiek het mogelijk maakt een Ubuntu-userspace op te starten op een Linux-kernel.

In een ander experiment bouwde Claude in Rust een interpreter voor een groot deel van Python en bewees het met de verificatietool Verus dat deze zich houdt aan de CPython-semantiek zoals beschreven in een academisch artikel. In de technische bijlage staat dat alle 17 lagen van de interpreter zijn bewezen, met als stelling: “Wanneer de interpreter een resultaat retourneert, is dat resultaat het resultaat dat de formele semantiek voorschrijft.” Anthropic zei dat empirische tests met 1,7 miljoen willekeurig gegenereerde Python-programma’s in 99,95% van de tests identiek gedrag aan CPython opleverden; van de zeven opzettelijk geïnjecteerde bugs bleven er vijf onopgemerkt bij willekeurige tests, terwijl ze alle zeven het bewijs ongeldig maakten.

Om de efficiëntie te meten, bouwde Anthropic 36 kleine verificatietaken door echte OSS-Fuzz-invoerpuntprogramma’s te verkleinen. Dat leverde programma’s op van 283–2.491 instructies, met invoer van maximaal 64 bytes en met AddressSanitizer vervangen door een ‘mini-ASan’-runtime van ongeveer 100 instructies. Volgens Anthropic bewijst Opus 5.5 de helft van de taken met ongeveer 40% minder tokens dan Opus 5. Anthropic meldt ook dat agents die elkaars bewijzen mochten kopiëren in een gedeelde werkruimte 17% minder tokens nodig hadden dan agents die alleen werkten, dat sommige agents slaagden nadat ze eerder alleen waren gezakt, en dat agents die alleen werkten er niet in slaagden twee van de bewijzen te voltooien. Het bedrijf zei dat hetzelfde hergebruikseffect op grotere schaal zichtbaar was tijdens het OSS-Fuzz-project: teams van agents kopieerden voltooide bewijzen en pasten die aan, omdat een groot deel van elk bewijs betrekking heeft op gedeelde initialisatiecode voor de C-runtime en AddressSanitizer.

Vermelde beperkingen en het OSS Verify-programma

Anthropic stelt dat de bewijzen niet betekenen dat de bibliotheken bugvrij zijn: resterende bugs kunnen zich in de vertrouwde componenten bevinden of buiten het bereik van de bewijzen vallen. De bewijzen gelden voor statische RISC-V-binaries met één thread die zijn gekoppeld aan musl libc, terwijl de meeste gebruikers deze bibliotheken op x86 of ARM gebruiken en ze dynamisch koppelen aan glibc. Bovendien detecteert AddressSanitizer niet alle bugs die de geheugenveiligheid in gevaar brengen. Het bedrijf zei te verwachten dat deze beperkingen beheersbaar worden naarmate modellen beter worden.

Theorem biedt via het programma OSS Verify dezelfde pijplijn gratis aan in aanmerking komende opensourceprojecten aan. Aanmelden kan via een pull request waarin de bestanden project.yaml, Dockerfile en build.sh aan de repository van het programma worden toegevoegd. Theorem zegt dat het projecten beoordeelt volgens vergelijkbare criteria als OSS-Fuzz, waarbij prioriteit wordt gegeven aan veelgebruikte kritieke infrastructuur. Volgens Theorem ontvangen beheerders een Rocq-bewijs, gecontroleerd door de Rocq-kernel, dat elk fuzzdoel niet crasht bij invoer tot 64 MiB; bugs die tijdens het bewijsproces worden gevonden, worden per e-mail vertrouwelijk aan beheerders gemeld, zonder deadline voor openbaarmaking, en het kan meerdere dagen duren om bewijzen te produceren. De routekaart van Theorem is erop gericht het volledige Nix-ecosysteem te verifiëren, met inbegrip van kritieke infrastructuur zoals glibc, OpenSSL en cURL.