Hvad der faktisk blev bevist
Anthropics Frontier Red Team offentliggjorde den 22. oktober sammen med Theorem resultater fra et forsøg på at bruge Claude til formel verifikation i stor skala. Holdet tog eksisterende fuzztest fra Googles OSS-Fuzz, behandlede hver test som en egenskab, koden skal opfylde, oversatte den til RISC-V-assembler og lod Claude skrive maskinkontrollerede beviser for, at den resulterende binær aldrig går ned.
Egenskaben er snæver og præcis: for ethvert input under 64 MB går programmet ikke ned med en hukommelsessikkerhedsfejl eller en fejlet påstand. Beviserne forudsætter en entrådet statisk binær med fast hukommelsesbudget på en RISC-V-processor under Linux, og de stoler på beviskontrollen Rocq, Theorems semantik for RISC-V og Linux-processer samt hardwaren og OCaml-oversætteren nedenunder.
Tallene
I 123 åbne biblioteker beviste Claude, at 239 indgangspunkter er fri for nedbrud under den specifikation. Beviserne fylder i alt omkring 180 millioner linjer Rocq. Et typisk bevis er cirka 600.000 linjer mod en medianlængde på omkring 18.000 RISC-V-instruktioner i binæren. Arbejdet tog nogle uger.
Anthropic oplyser ikke, hvor mange indgangspunkter der blev forsøgt i alt, så tallene giver ingen succesrate. Selskabet siger, at det offentliggør beviser for de fuzztest, der ikke krævede en rettelse, og specifikationer for dem, det ikke kunne bevise.
Hundredvis af fejl dukkede op undervejs, og Claude rettede dem, hvilket genskabte specifikationerne. Eksemplerne omfatter et tællerunderløb i en dekomprimerer, der kun giver en skrivning uden for grænserne ved en sjælden opstilling på omkring 20 MB input, en læsning uden for grænserne i en billeddekoder, der kræver 64 MB input og mere end 2 GB hukommelse, og en genopdagelse af CVE-2026-56132 i libexpat. Én var en filbegrænsning, der ikke altid blev håndhævet: en logisk fejl, der aldrig går ned, og som havde ligget latent i mere end ti år.
Den åbenlyse genvej, og hvad de gjorde ved den
Opstillingen har et hul, holdet selv peger på. Claude kunne gøre et teorem bevisbart ved at skrive programmet om, så det aldrig gik ned. Anthropic oplyser, at man straffede rettelser, der ændrede adfærd, gav ekstra kredit for at bevise, hvilke input en rettelse ændrer, og loggede og reviderede hver rettelse.
Omkostningen er det åbne problem
På en test med 36 små verifikationsopgaver bygget af ægte OSS-Fuzz-kode, med tre uafhængige forsøg og et budget på fem millioner tokens hver, beviste Opus 5.5 halvdelen med omkring 40 procent færre tokens end Opus 5. Agenter, der måtte kopiere hinandens beviser fra et delt arbejdsrum, brugte 17 procent færre tokens og fuldførte 34 af de 36 mod 32 for agenter, der arbejdede alene.
Anthropic er tydelig om begrænsningerne. »Formelt verificeret« betyder ikke fejlfri: en beviskontrol kan ikke bekræfte, at specifikationen svarer til virkeligheden, og fejl kan blive tilbage i specifikationen, maskinmodellen eller den betroede base. Beviserne dækker RISC-V-binærer linket mod musl, mens de fleste installationer kører x86 eller ARM med dynamisk linket glibc. Og et enkelt bevis kan koste hundredvis af millioner tokens, hvilket selskabet kalder et centralt åbent problem.
Separat skrev Claude en specifikation ud fra RFC 1950 og beviste, at Linux-kernens zlib-implementering opfylder den på x86-binærniveau. Anthropic siger, at man gentog det for omkring seks andre udbredte biblioteker. Om det x86-arbejde lader sig generalisere videre, er det, der bør følges.
