AlphaProof-kod bevisade att Signals krypto är korrekt – på nivå med den kompilerade binären

Sex och en halv miljon rader Lean, producerade på fyra veckor av agentteam som ingen människa hjälpte att skriva. Det är siffran i rubriken som G​oogle DeepMind publicerade den 10 november 2026 för AlphaProof Code, ett agentiskt ramverk för formell verifiering som labbet använde för att maskinverifiera den kryptografiska kärnan i Signal-protokollet – och, ovanligt nog, för att verifiera den på nivån för den kompilerade AArch64-binären i stället för designdokumentet ovanför den. Modellerna som utförde arbetet är en annan fråga. en API-nyckel till leverantörens listpris med 0 % påslag Bevisagenternas motor är inte något vi tillhandahåller.

Ramverket är inte en modell som du kan anropa. Det är en rigg: mänskliga experter avgör vad som måste vara sant, en blandning av modeller omvandlar dessa mål till Lean-specifikationer och sedan fyller team av bevisskrivande agenter – bloggen namnger Gemini Carbon som motorn – i bevisen tills Lean-kärnan accepterar dem. Det som släpptes tillsammans med tillkännagivandet är artefaktuppsättningen på github.com/google-deepmind/code-verification och en teknisk artikel som är betydligt mer uppriktig om resultatets gränser än blogginlägget är. Det mesta av det som följer kommer från den artikeln, eftersom det är där de intressanta siffrorna finns.

Vad bevisades egentligen, och mot vad?

Målet är libsignal v0.105.4 med spqr v1.6.0, byggt med standard-rustc 1.98.1, statiskt länkat mot musl och emitterat som en enda körbar AArch64 Linux-fil. Den detaljen är viktigare än något benchmarkresultat: bevisen handlar om de byte som skulle köras på en telefon, inte om en Rust-funktion som förväntas bli troget översatt av en kompilator. Teamet verifierade ungefär 560 KB libsignal-källkod, cirka 140 000 AArch64-instruktioner, och de gjorde det genom att skriva en Lean-modell över instruktionsuppsättningen – 467 instruktioner och 31 systemanrop, på 7 578 rader – och sedan bevisa att den verkliga ELF-avbilden, när den laddas och körs under den modellen, bevarar säkerhetsegenskaperna.

Egenskaperna är de som en protokollingenjör skulle efterfråga. Tio symboliska satser täcker framåtsekretess, säkerhet efter kompromettering, sekretess för initiativtagare och svarare, autentisering och fem följdsatser till PQXDH:s sats 1. Huvudresultatet heter signal_session_secure_placed. Det finns också ett beräkningsspår med en konkret gräns, och de två spåren använder olika motståndarmodeller: den symboliska sidan (Dolev–Yao, via ramverket DyLean) täcker till och med en kvantangripare som bryter Diffie–Hellman efter handskakningen, medan den beräkningsmässiga sidan endast täcker klassiska motståndare.

Vart de sex miljoner raderna tar vägen

”Över sex miljoner rader” är bloggens formulering, och den är korrekt men grov. Artikelns uppdelning är den användbara, och den är värd att läsas som en kostnadstabell snarare än som ett skryt:

• Bevis för binären — 5,3 miljoner rader, huvuddelen av arbetet, som täcker maskinkodens semantik och förfiningen från den symboliska modellen ned till det körbara programmet.

• Beräkningsbevis — cirka 860 000 rader.

• Symboliska bevis — cirka 350 000 rader.

• Bevis som motbevisar buggar — cirka 140 000 rader, för de två avsiktligt återinförda sårbarheterna som beskrivs nedan.

• Allokatorbevis — cirka 70 000 rader.

Nästan sju miljoner rader om man räknar kommentarer och tomrader, vilket artikeln gör men bloggen inte. Hur som helst är det förhållande som spelar roll det mellan beviset och det som bevisas: 6,5 miljoner rader Lean för att fastställa egenskaperna hos en binärfil på 560 KB. Det förhållandet är det ärliga måttet på hur långt den här tekniken är från att vara rutinmässig, och det är siffran att citera när någon frågar om formell verifiering har blivit billig.

Den betrodda basen är mindre än beviset, och det är själva poängen.

Ett bevis är bara så bra som sina antaganden. Artikeln är specifik om detta, och specificiteten är det som skiljer den från ett pressmeddelande. De betrodda specifikationerna omfattar cirka 18 000 rader (28 000 med dokumentation), AArch64-semantiken cirka 8 000 och Lean-kodningen av maskinkoden runt 95 000. Trettiosju rutiner ersätts av kontrakt i stället för att verifieras – SHA-256- och SHA-512-komprimering, AES-256-CBC, X25519, Edwards-kurvoperationerna, Kyber1024 och ML-KEM-768 samt libcrux HMAC. Arton panik-ingångspunkter antas likaså i stället för att bevisas.

Så påståendet är inte "allt är bevisat." Påståendet är att den kryptografiska protokollogiken, sessionstillståndsmaskinen och förfiningen från den logiken till de instruktioner som faktiskt körs är bevisade, medan primitiverna under dem är betrodda på det sätt som varje verifieringsprojekt betror sina primitiver. Rust-kompilatorn är, märk väl, inte i den betrodda basen – teamet undvek att behöva betro den genom att resonera på maskinkodsnivå, vilket är samma knep som låter dem kringgå en verifierad kompilator helt och hållet. För kontext om skalan citerar artikeln seL4 på ungefär 20 personår och CompCert på omkring 6.

Två buggar, medvetet återinförda

Ett verifieringssystem som bara någonsin säger "korrekt" går inte att testa. Därför tog teamet två sårbarheter som tidigare hade hittats och åtgärdats i Signals kod — en bugg med svagt tillstånd och en bugg med liten undergrupp — återinförde dem i en isolerad kopia och körde om pipelinen. I båda fallen producerade AlphaProof Code ett maskinkontrollerat bevis för att den buggiga versionen inte uppfyller säkerhetsteoremet: det symboliska påståendet reduceras till ¬Sec(Asm_bug).

Artikeln lägger till en brasklapp som en marknadsföringssida skulle ha skurit bort: att vederlägga den beräkningsmässiga satsen för de buggarna är "mycket svårare" och lämnades som en öppen fråga. Med andra ord fungerar det negativa testet rent på det symboliska spåret och fungerar ännu inte på det beräkningsmässiga. Det är precis den typen av asymmetri som en läsare bör känna till innan hen behandlar ramverket som en buggdetektor.

Hur agenterna kördes

Fem forskare under fyra veckor, var och en körande agenter oavbrutet. Själva bevisförfattandet gjordes av team på 40 till 80 agenter, som körde mellan 24 och 72 timmar på en enda maskin per team, med en övervakande agent ovanför teamets orkestrerare. En grindvaktsagent kontrollerar varje inlämning med jämförare mot en undanhållen kopia av specifikationen och mot Leans kärna – ett skydd mot att en agent bevisar en subtilt försvagad version av det som efterfrågades.

Det mänskliga arbetet var koncentrerat till början, på specifikationerna. Varje specifikation granskades av en expert innan bevisarbetet började, och agenternas egen granskningsomgång flaggade omkring 1 % av kodbasen för mänsklig uppmärksamhet. Ingen människa skrev beviskod. Artikeln är också uppriktig om ingenjörsarbetet: en ren build kan ta flera timmar, tidigt kunde en mindre källkodsändring eller en omkompilerad binärfil tvinga fram omfattande reparationer av bevisen, och det finns "stort utrymme för optimering" i både de AI-genererade bevisen och själva bevisteknikerna.

Vad bevisen inte täcker

Begränsningarna är tillräckligt omfattande för att vara den viktigaste delen av artikeln, och de anges tydligt. Ingen postkvantgaranti fastställs för SPQR:s läkande egenskap – ratchet-teoremen förutsätter att angriparen väljer SPQR-nycklar. Nyttolastens sekretess bevisas inte. Svararens autentisering bevisas inte för det första meddelandet i en handskakning som aldrig befordras. Modellen tillåter en session per befordran, fasta meddelandelängder, inget tillstånd för flera enheter och identitetsnycklar med tillit vid första användning.

Det finns också en gräns som blir intetsägande. Termen för 8-byte-MAC-förfalskning är minst 2⁻⁶⁴ per försök och växer kvadratiskt i meddelanden och epoker, vilket innebär att gränsen slutar säga något för en enda session på ungefär 25 000 meddelanden, eller för 2²⁰ sessioner med 2¹⁰ meddelanden. Och föremålet för beviset är teamets bygge av libsignal-cli som körs som en ny process — inte Signal-appen på din telefon. Flera miljöantaganden argumenteras informellt i stället för att bevisas.

Det finns inget API, inget pris och ingen modell att anropa

Det här är delen som kommer att göra alla som kommer från en modelltopplista besvikna. AlphaProof Code är ett forskningsramverk och en publicerad uppsättning artefakter. Det finns ingen endpoint, ingen prislista per token, ingen väntelista och inga vikter: arkivet innehåller Lean-utvecklingen, AArch64-semantiken, libsignal-bindningen och specifikationerna, inte en checkpoint. Bloggen säger att artefakterna är öppna med öppen källkod; landningssidan anger ingen licens, vilket är värt att kontrollera innan någon planerar att bygga vidare på dem.

Vilka modeller som utförde arbetet är en annan fråga. Rapporten namnger G​emini 4 Carbon för bevisagenterna och anger att Claude Opus 5.5 användes tillsammans med andra modeller för att utarbeta och granska specifikationer. Claude Opus 5.5 finns i OrcaRouters katalog i dag för 4 USD per miljon indatatokens och 20 USD per miljon utdatatokens, med leverantörens listpris vidarefakturerat utan påslag (0 % påslag) — så om den praktiska slutsatsen du vill ha är "kör en loop för att utarbeta specifikationer med modellen som rapporten använde", är den delen ett vanligt API-anrop, och en ändring av leverantörens pris slår igenom hos oss samma dag. Bevisagenternas motor är inte något vi tillhandahåller, och inget här antyder att vi själva driftar AlphaProof Code.

Varför detta är en större sak än Signal-resultatet

Signal-verifieringen är imponerande i sig — den första formella verifieringen av implementeringen av ett protokoll som används i stor utsträckning, med vilken metod som helst, med eller utan AI, enligt DeepMind, och första gången AI har verifierat ett driftsatt kryptografiskt protokoll på denna nivå. Men det överförbara påståendet är arbetsflödet. Ett team på fem personer, på fyra veckor, med ett specifikationsgranskningssteg och en agent som grindvakt, producerade en beviskorpus som tidigare skulle ha varit ett projekt på flera år. Om den kvoten håller ens löst förändras uppsättningen system som har råd med verifiering: firmware för medicintekniska enheter, programvara för elnät, den sorts kod som för närvarande får en kodgranskning och en bön.

Huruvida det håller är otestat. Signals kryptografi är ovanligt väl specificerad, teamet lät Signals egna ingenjörer granska metodiken, och primitiverna upphandlades externt i stället för att verifieras. Nästa system kommer inte att vara lika tillmötesgående. Artikelns egen inramning – att kombinera formell verifiering med automatiserade försvarsagenter som CodeMender – är den ärliga formen av pitchen: verifiering talar om vad som är sant, och något annat måste åtgärda det som inte är det.

Vad du ska titta på

Tre saker skulle flytta detta från en banbrytande artikel till en industriell teknik. En andra, oberoende kodbas verifierad av någon utanför Google, helst en där specifikationen måste skrivas från scratch i stället för att anpassas från en befintlig analys. En kostnadssiffra – agenttimmar, acceleratortimmar, dollar – eftersom fyra veckor och team med 40 till 80 agenter inte är en enhet som någon ingenjörschef kan budgetera efter. Och buggmotbevisningen på beräkningsspåret, som artikeln lämnar öppen och som är skillnaden mellan ett system som bevisar egenskaper och ett system som också beräkningsmässigt kan säga att en specifik binärfil är trasig.

Tills dess, läs artefaktarkivet i stället för tillkännagivandet. Bevisen finns där, Lean kontrollerar dem, och artikeln berättar exakt vad de förutsätter.