Vad som faktiskt bevisades
Anthropics Frontier Red Team publicerade den 22 oktober, tillsammans med Theorem, resultat från ett försök att använda Claude för formell verifiering i stor skala. Laget tog befintliga fuzztester från Googles OSS-Fuzz, behandlade varje test som en egenskap koden måste uppfylla, kompilerade det till RISC-V-assembler och lät Claude skriva maskinkontrollerade bevis för att den resulterande binären aldrig kraschar.
Egenskapen är snäv och precis: för varje indata under 64 MB kraschar programmet inte med ett minnessäkerhetsfel eller ett misslyckat villkor. Bevisen förutsätter en enkeltrådad statisk binär med fast minnesbudget på en RISC-V-processor under Linux, och de litar på beviskontrollanten Rocq, Theorems semantik för RISC-V och Linux-processer samt hårdvaran och OCaml-kompilatorn under dem.
Siffrorna
I 123 öppna bibliotek bevisade Claude att 239 ingångspunkter är fria från krascher under den specifikationen. Bevisen omfattar sammanlagt ungefär 180 miljoner rader Rocq. Ett typiskt bevis är omkring 600 000 rader, mot en medianlängd på cirka 18 000 RISC-V-instruktioner i binären. Arbetet tog några veckor.
Anthropic uppger inte hur många ingångspunkter som försöktes totalt, så siffrorna ger ingen träffkvot. Bolaget säger att det publicerar bevis för de fuzztester som inte behövde någon patch, och specifikationer för dem det inte kunde bevisa.
Hundratals buggar dök upp på vägen, och Claude patchade dem, vilket återskapade specifikationerna. Exemplen omfattar ett underflöde i en räknare i en dekomprimerare som ger en skrivning utanför gränserna endast vid en ovanlig layout om cirka 20 MB indata, en läsning utanför gränserna i en bilddekodare som kräver 64 MB indata och mer än 2 GB minne, samt ett återupptäckt CVE-2026-56132 i libexpat. En var en filbegränsningsfunktion som inte alltid upprätthölls: en logikbugg som aldrig kraschar och legat latent i mer än ett decennium.
Den uppenbara genvägen, och vad de gjorde åt den
Uppställningen har ett hål som laget själv pekar ut. Claude kunde göra ett teorem bevisbart genom att skriva om programmet så att det aldrig kraschar. Anthropic uppger att man straffade patchar som ändrade beteende, gav extra poäng för att bevisa vilka indata en patch påverkar, samt loggade och granskade varje patch.
Kostnaden är det öppna problemet
På ett test med 36 små verifieringsuppgifter byggda av riktig OSS-Fuzz-kod, med tre oberoende försök och en budget på fem miljoner tokens vardera, bevisade Opus 5.5 hälften med omkring 40 procent färre tokens än Opus 5. Agenter som fick kopiera varandras bevis från en delad arbetsyta använde 17 procent färre tokens och klarade 34 av de 36, mot 32 för agenter som arbetade ensamma.
Anthropic är tydligt med begränsningarna. ”Formellt verifierad” betyder inte buggfri: en beviskontrollant kan inte bekräfta att specifikationen motsvarar verkligheten, och buggar kan finnas kvar i specifikationen, maskinmodellen eller den betrodda basen. Bevisen täcker RISC-V-binärer länkade mot musl, medan de flesta driftsättningar kör x86 eller ARM med dynamiskt länkad glibc. Och ett enda bevis kan kosta hundratals miljoner tokens, vilket bolaget kallar ett centralt öppet problem.
Separat skrev Claude en specifikation utifrån RFC 1950 och bevisade att Linuxkärnans zlib-implementation uppfyller den på x86-binärnivå. Anthropic uppger att man upprepat det för ungefär sex andra vanliga bibliotek. Om det x86-arbetet går att generalisera vidare är det som bör följas.
