Anthropic meddelade att företagets Claude-modell kan ta fram formella verifieringsbevis för befintlig kod automatiskt. I ett test med 123 bibliotek från Googles OSS-Fuzz-projekt genererade Claude omkring 180 miljoner rader bevis på några veckor. Bevisen kontrollerades av verifieraren Rocq, och enligt Anthropic krävdes nästan ingen mänsklig granskning.
Vad systemet faktiskt gjorde
Claude skrev inte nya program. I stället omvandlade modellen kraschtester till matematiska påståenden, analyserade den kompilerade maskinkoden och tog fram formella bevis för att koden uppfyller påståendena. När modellen stötte på en bugg fick den rätta koden själv. Under en veckas granskning av en populär PDF-läsare hittade Claude lika många säkerhetsbuggar som brukar rapporteras under ett helt år. I ett annat bibliotek hittade modellen ett logiskt fel som hade varit dolt i mer än tio år.
Begränsningar och kostnader
Anthropic betonar att bevisen bara gäller för program med en tråd som körs på en viss processorarkitektur och med indata på under 64 MB. Beräkningsbehovet är stort – enskilda bevis kräver hundratals miljoner token – men företaget uppgav inte den totala kostnaden. Ett mindre test visade att den nyare modellen Opus 5.5 kan ta fram hälften av bevisen med omkring 40 % färre token än föregångaren.
Varför det spelar roll
Om AI kan verifiera kod automatiskt kan utvecklare lägga mindre tid på att leta efter buggar och granska kodändringar, särskilt i säkerhetskritisk programvara. Den nuvarande metoden fungerar dock bara med strikta begränsningar för hårdvara och indata, så traditionella tester behövs fortfarande för de flesta vanliga program.
