Anthropic zegt dat Claude formele bewijzen schreef dat 123 opensourcebibliotheken niet kunnen crashen

In een samenwerking met Theorem zegt Anthropic Claude te hebben gebruikt om beveiligingseigenschappen op assemblyniveau (RISC-V) te bewijzen in meer dan 100 opensourcebibliotheken uit de praktijk. Het noemt dit het eerste grootschalige gebruik van AI om productiesoftware op dat niveau formeel te verifiëren.

Volgens Anthropic:

• Wat is bewezen: voor 239 fuzz-testingangspunten in 123 OSS-Fuzz-bibliotheken eindigen de programma's altijd normaal, zonder fouten in de geheugenveiligheid of mislukte assertions, voor elke invoer onder 64 MB. Dit geldt onder bepaalde aannames: een statische binary met één thread en een vast geheugenbudget, op een RISC-V-CPU met Linux. De bewijzen beslaan in totaal ongeveer 180 miljoen regels Rocq, gecontroleerd door de Rocq-proofchecker.
• Hoe: de bestaande fuzz-test van elke bibliotheek werd omgezet in een specificatie (