Anthropic presenterte resultatene av eksperimenter som brukte AI-modeller for å formelt verifisere påliteligheten og sikkerheten til eksisterende prosjekter. Under eksperimentet ble AI-modeller brukt til å generere matematiske bevis på fraværet av minnefeil for 123 åpen kildekode-biblioteker testet i OSS Fuzz-infrastrukturen.
Verifiseringen ble utført på kompilert assemblerkodenivå for RISC-V-arkitekturen. Det totale volumet av genererte bevis utgjorde omtrent 180 millioner kodelinjer for Rocq Prover-verifiseringssystemet (omtrent 600 000 linjer per binærfil med 18 000 RISC-V-instruksjoner). Bevisene ble generert ved automatisk å konvertere eksisterende fuzzing-tester til formelle spesifikasjoner, hvoretter Claude AI-modellen beviste at programmet er feilfritt for alle inngangsdata opptil 64 MB.
Under bevisbyggingsprosessen var AI-modellen i stand til å identifisere og forberede rettelser for hundrevis av feil som tidligere ikke var oppdaget av fuzz-testing. Blant annet inkluderte disse sårbarheter for bufferoverløp ved behandling av visse inndata (f.eks. CVE-2026-56132 i libexpat), samt logiske feil. Videre ble AI-modellen brukt til å bevise samsvar med kjernens implementering av zlib-algoritmen. Linux RFC 1950-spesifikasjoner.
En tolk for et delsett av Python ble også generert i Rust, og for dette ble det utarbeidet et formelt bevis på samsvar med CPython-semantikk ved hjelp av Verus-verktøysettet. For å sammenligne oppførsel med CPython ble over 1.7 millioner tilfeldig genererte Python-programmer kjørt. I 99.95 % av tilfellene samsvarte resultatene av å kjøre disse programmene i den nye implementeringen og i CPython, og eventuelle avvik som ble funnet var kjente kanttilfeller.
Formell verifisering garanterer samsvar med spesifikasjonene, men det eliminerer ikke sikkerhetsproblemer fullstendig, ettersom risikoer forårsaket av flertrådsproblemer, dynamisk lenking og unormal oppførsel på ekte maskinvare forblir uformalisert. En viktig fordel med den foreslåtte tilnærmingen er at den fungerer direkte med binære filer, noe som eliminerer behovet for å omskrive eksisterende kode i formelt verifiserbare språk.
Kilde: opennet.ru
