Anthropic zegt dat Claude heeft bewezen dat 123 open-sourcebibliotheken niet kunnen crashen

Anthropic zegt dat Claude wiskundig heeft bewezen dat fuzz-geteste code in 123 open-sourcebibliotheken niet kan vastlopen bij invoer kleiner dan 64 MB, en dat er daarbij bugs zijn gevonden die door jarenlange tests over het hoofd waren gezien.

Het werk, uitgegeven door Anthropic op 22 oktober In samenwerking met de startup Theorem, gespecialiseerd in formele verificatie, worden 239 ingangspunten van Google's OSS-Fuzz-project behandeld. Anthropic noemt het de eerste grootschalige poging om AI te gebruiken voor de formele verificatie van productiesoftware op het niveau van de assembleercode.

Van tests tot bewijzen

Bij fuzzing worden enorme aantallen willekeurige invoerwaarden aan een programma aangeboden om te zien wat er misgaat, maar het kan nooit elke mogelijke invoerwaarde uitproberen. Anthropic heeft elke bestaande fuzz-test omgezet in een formele regel, "deze test zal nooit crashen", en Claude heeft bewezen dat dit geldt voor elke invoerwaarde kleiner dan 64 MB.

De bewijzen werken met gecompileerde RISC-V-machinecode in plaats van broncode. In een paar weken tijd schreef Claude ongeveer 180 miljoen regels bewijs in de Rocq-bewijsassistent, zo'n 600.000 regels voor een typisch programma. Niemand hoeft ze te lezen; de Rocq-controleur bevestigt ze stuk voor stuk automatisch.

Testen op bugs gemist

Telkens als een bewijs mislukte, had Claude een fout gevonden, deze verholpen en het opnieuw geprobeerd. Anthropic zegt dat de inspanning honderden fouten aan het licht bracht, waaronder een out-of-bounds schrijffout in een decompressor die alleen voorkwam bij invoer van ongeveer 20 MB met één zeldzame lay-out, en de herontdekking van een bekende fout in de libexpat XML-parser.

In afzonderlijke tests bewees Claude dat de zlib-code van de Linux-kernel overeenkomt met de specificatie van het formaat. Tijdens het controleren van een veelgebruikte PDF-lezer ontdekte hij in één week evenveel beveiligingslekken als er normaal gesproken in een jaar worden gemeld. Meer details zijn te vinden in de technische bijlage.

Wat het niet bewijst

Anthropic maakt expliciet dat "formeel geverifieerd" niet betekent dat het bugvrij is. De bewijzen gaan uit van single-threaded, statisch gelinkte RISC-V-binaries op Linux, terwijl de meeste implementaties in de praktijk op x86 of ARM draaien. De gebruikte geheugencontroles vangen niet elke geheugenveiligheidsbug op, en niet elk toegangspunt in elke bibliotheek is gecontroleerd.

De kosten vormen een ander addertje onder het gras: bewijzen kunnen honderden miljoenen tokens kosten. Anthropic zegt dat Claude Opus 5.5 de helft van een benchmark met 36 taken heeft opgelost met ongeveer 40% minder tokens dan Opus 5, en dat agents die bewijzen deelden 17% minder tokens gebruikten.

Waarom het belangrijk is

AI wordt steeds beter in het vinden van bugs, omdat de PHP2Shell-fouten liet deze week zien. Bewijzen zijn een manier om aan te tonen dat hele categorieën bugs simpelweg niet bestaan. Theorem heeft een Claude vaardigheid voor open-source beheerders die hun projecten willen registreren, en het schattingen dat 95% aan machinecode in het Nix-software-ecosysteem tegen het einde van 2027 geverifieerd zou kunnen worden, wat neerkomt op ongeveer $134 miljoen.