Kort fortalt

  • Anthropic rapporterer bevis mot bestemte krasj for 239 testinnganger i 123 OSS-Fuzz-biblioteker.
  • Bevisene gjelder éntrådede RISC-V-programmer, modellert Linux, fast minnebudsjett og inndata under 64 MiB – ikke feilfrie biblioteker.
  • Det publiserte delutvalget dekker 60 testinnganger i 25 biblioteker og utelukker ikke kjøringer som aldri avsluttes.

Gjør eksisterende tester om til matematiske krav

Anthropic og Theorem opplyser at Claude har skrevet bevis mot krasj for 239 testinnganger i 123 åpne kodebiblioteker fra OSS-Fuzz. Modellen fant og rettet også feil underveis, ifølge selskapets gjennomgang publisert 22. oktober.

En testinngang er en bestemt vei inn i koden som utviklerne bruker til testing. Ved såkalt fuzzing sender et testverktøy store mengder varierte inndata gjennom denne inngangen for å lete etter feil. I forsøket ble testene i stedet gjort om til matematiske krav som beviskontrolløren Rocq kunne kontrollere.

Bevisene gjelder ferdig kompilerte programmer, ikke bare kildekoden slik den er skrevet. Resultatene for det større forsøket er rapportert av Anthropic, ikke en uavhengig gjentakelse utført av KIavisa.

Gjelder bestemte maskin- og minnevilkår

Forsøket gjelder éntrådede, statiske programmer for prosessorarkitekturen RISC-V, med C-biblioteket musl og et fast minnebudsjett. Programmene er beskrevet i en matematisk modell av Linux. Bevisene forutsetter at denne modellen og de andre betrodde delene er korrekte.

Det tekniske vedlegget avgrenser inndata til under 64 MiB. I det offentliggjorte bevisutvalget avvises inputfiler på 64 MiB eller mer før selve testinngangen kalles. Oppgitt minnebudsjett er også et premiss, slik at inndata som krever mer minne ikke omfattes.

Anthropic understreker at dette ikke gjør hele bibliotekene feilfrie. Ikke alle testinnganger er verifisert, og minnekontrollverktøyet AddressSanitizer oppdager ikke alle minnefeil. Feil bruk av biblioteket fra andre programmer ligger også utenfor den avgrensede garantien.

Publiserer et mindre utvalg av bevisene

Det publiserte delutvalget omfatter 60 testinnganger i 25 biblioteker. Dokumentasjonen sier uttrykkelig at ingen av bevisene i denne utgivelsen utelukker en kjøring som aldri tar slutt. Krasjvern og et bevis for at programmet faktisk avslutter er ulike egenskaper.

Et korrekt bevis kan dessuten gjelde en modell som ikke samsvarer fullt ut med virkeligheten. Theorems dokumentasjon presiserer at kontroll av systemkallenes formelle spesifikasjon ikke i seg selv viser at spesifikasjonen stemmer med virkelig Linux.

Flere kilder

Kilder og åpenhet

Sammendraget bygger på opplysninger fra Anthropic og Theorem, publisert 22. oktober 2026 · klokkeslett ikke oppgitt. Les kilden for alle detaljene og eventuelle senere oppdateringer.

Les originalkilden hos Anthropic og Theorem

Vi har skrevet sammendraget med hjelp fra KI. Vi har ikke selv testet leverandørens påstander eller resultater. Bildet er en illustrasjon, ikke dokumentasjon av produktet eller hendelsen. Slik bruker vi kilder.