Google DeepMind meddelade den 10 nov 2026 att deras nya AI-ramverk, AlphaProof Code, hade använts för att formellt verifiera den faktiska koden i Signal-protokollet. Formell verifiering innebär att man matematiskt bevisar att programvara fungerar precis som avsett, utan dolda buggar. Teamet vägledde AI-agenter i att ta fram och kontrollera ett bevis för att den kompilerade Signal-koden upprätthåller centrala säkerhetsgarantier, till exempel att meddelanden förblir skyddade även om en enhet tillfälligt komprometteras. Hela arbetet tog fyra veckor – en uppgift som normalt skulle kräva flera års arbete från expertteam.
Det här gör AlphaProof Code
AlphaProof Code är ett agentbaserat system med flera stora språkmodeller (LLM). Mänskliga forskare översätter först Signals säkerhetsmål till formella specifikationer och granskar varje steg. Därefter skriver en grupp agenter, som drivs av DeepMinds modell Gemini Carbon, beviset i Lean, ett språk som kontrollerar matematiska satser. Agenterna producerade över sex miljoner rader Lean-kod och flaggade bara omkring en procent av kodbasen för mänsklig granskning. Systemet identifierade också korrekt två tidigare åtgärdade buggar när de återinfördes, vilket visar att det kan skilja säker kod från kod med buggar.
Därför är det viktigt
Verifieringen omfattar den kompilerade implementationen, inte bara utformningen, och täpper därmed till en lucka där många sårbarheter i verkliga system döljer sig. Signals teknikchef, Ehren Kret, sade att resultatet ger ”större förtroende för våra kodbaserade integritetsgarantier”. Experter ser detta som ett steg mot att använda AI för att ge avancerad säkerhetsgranskning av banker, medicintekniska produkter, programvara för elnät och andra kritiska system.
Varför det spelar roll
För vanliga användare innebär arbetet att krypteringen som skyddar miljarder meddelanden i Signal och Google Messages har kontrollerats matematiskt på implementationsnivå, vilket minskar risken för dolda brister. För utvecklare visar det en praktisk väg att använda AI-stödd formell verifiering för att påskynda säkerhetsgranskningar, även om det fortfarande är oklart hur metoden kan skalas upp och vad den kostar.
