Claude bewijst wiskundig dat 123 codebibliotheken niet crashen

Anthropic heeft Claude wiskundige bewijzen laten schrijven voor de veiligheid van 123 veelgebruikte opensourcebibliotheken. Dat meldt het Frontier Red Team van het bedrijf in een onderzoeksverslag van 22 oktober. Het werk gebeurde samen met de Amerikaanse start-up Theorem, die zich specialiseert in automatische formele verificatie.

Wat Claude precies heeft bewezen

Bij formele verificatie test je software niet met voorbeelden, je bewijst met wiskunde dat een eigenschap altijd geldt. Anthropic koos als eigenschap: het programma crasht niet, bij welke invoer tot 64 MB dan ook. Dat dekt geheugenfouten en mislukte controles die de tool AddressSanitizer opspoort.

Het team zette bestaande fuzztests uit Googles OSS-Fuzz om in specificaties voor gecompileerde RISC-V-code. Claude schreef de bewijzen, de proof checker Rocq (voorheen Coq) controleerde ze. In totaal gaat het om 239 ingangspunten en zo’n 180 miljoen regels Rocq. Een gemiddeld bewijs telt ongeveer 600.000 regels. Volgens Anthropic kostte dit “een paar weken”. Ter vergelijking noemt het bedrijf de seL4-microkernel, waarvan de verificatie ooit twintig persoonjaren vergde.

Bugs die jarenlang onopgemerkt bleven

Tijdens de bewijspogingen kwamen honderden fouten boven. Een paar voorbeelden uit het verslag: een tellerfout in een decompressor die tot een schrijfactie buiten het geheugen leidde (alleen bij een invoer van ongeveer 20 MB in een zeldzame opbouw), en een leesfout in een beelddecoder die pas optrad bij 64 MB invoer en meer dan 2 GB geheugen. In libexpat vond Claude opnieuw het lek CVE-2026-56132. In een veelgebruikte toepassing zat een logische fout die volgens Anthropic “meer dan tien jaar” latent was. Bij een niet nader genoemde pdf-lezer vond het team in één week evenveel beveiligingsbugs als er normaal in een jaar worden gemeld.

Claude repareerde de gevonden fouten ook zelf en bewees daarna opnieuw dat er geen crash meer mogelijk was. Om valsspelen te voorkomen (een programma dat nooit iets doet, crasht ook nooit) strafte het team patches die het gedrag veranderden en werden alle wijzigingen gelogd en gecontroleerd.

Dit sluit aan bij eerder werk van Anthropic, zoals de gratis scanner die opensourcecode doorlicht. Het verschil: een scanner zoekt naar fouten, een bewijs sluit een hele klasse fouten uit.

De kanttekeningen

Anthropic is er zelf duidelijk over: “Formeel geverifieerd betekent niet bugvrij.” De bewijzen gaan uit van een enkelvoudig draaiend RISC-V-programma met musl libc op Linux. De meeste computers draaien x86 of ARM met glibc. AddressSanitizer vangt ook niet alle geheugenfouten, en niet elk ingangspunt is meegenomen. Daarbij kost een bewijs soms honderden miljoenen tokens, wat de rekensom voor kleinere projecten lastig maakt.

Het nieuwere model helpt wel. Op 36 kleine taken bewees Claude Opus 5.5 de helft met ongeveer 40 procent minder tokens dan Opus 5. Theorem zet het project op de eigen site neer als bewijs dat formele verificatie “op veel grotere schaal haalbaar” wordt. The Neuron rekende het onderzoek vandaag tot het belangrijkste AI-nieuws van de dag.

Wat betekent dit

AI-modellen vinden momenteel sneller lekken dan beheerders ze kunnen dichten. Denk aan PHP2Shell of de uitgestelde release van PostgreSQL 19. Ook aanvallers gebruiken agents, zoals Microsoft deze week liet zien met de Storm-0940-campagne. Bewijzen dat code een bepaalde fout niet kan bevatten, is een verdediging die meeschaalt. Anthropic noemt in het verslag ook glibc, OpenSSL, cURL en de Linux-kernel. Voor gewone gebruikers verandert er voorlopig niets. Voor wie software bouwt, schuift de vraag op van “hebben we genoeg getest?” naar “wat hebben we bewezen?”