# AlphaProof Code og Signal: maskinkontrollerede sikkerhedsbeviser og betroede antagelser

Published: 2026-11-11

Google DeepMind rapporterer maskinkontrollerede beviser for udvalgte sikkerhedsegenskaber for en kompileret libsignal kommandolinje-harness. Lean kontrollerer beviset, mens mennesker godkender specifikationen og dens antagelser. En separat komparator kontrollerer teoremet og alle afhængige definitioner mod det godkendte mål.

Canonical: https://thedailydiff.dev/da/video/2026-11-10-signal-machine-proof/

## Hvad denne video dækker

- AI-agenter producerer kandidatbeviser; Leans kerne kontrollerer, om de etablerer den menneskegodkendte formelle påstand.
- Det verificerede mål er en bestemt kompileret libsignal CLI-harness, med betroet semantik og kryptografiske kontrakter.
- Bevis for det kompilerede binær fjerner Rust-kompileren fra den betroede base for det binærs angivne egenskaber.
- Forskere rapporterer to isolerede genindførsler af tidligere rettede fejl, der overtræder deres symbolske sikkerhedsteorem.
- Komparatoren kontrollerer teoremet og enhver afhængig definition mod en beskyttet godkendt specifikation; ændringer gennemgår en separat gennemgået proces.

## Spørgsmål og svar

### Hvad beviste AlphaProof Code om Signals implementering?

Google DeepMind rapporterer kontrollerede beviser for udvalgte sikkerhedsegenskaber for en kompileret libsignal kommandolinje-harness. Det tekniske papir dækker meddelelsesfortrolighed og -autentifikation, med forward secrecy og post-kompromitteringssikkerhed under angivne modeller. Resultatet bevarer betingelser for angriberen, sessionen og kryptografiske antagelser. Dets omfang udelukker en generel garanti for enhver Signal-applikation eller -installation.

### Hvem bestemmer, hvad et AI-genereret sikkerhedsbevis skal etablere?

Menneskelige anmeldere godkender specifikationen og dens antagelser. Google DeepMinds tekniske papir beskriver agenter, der udarbejder specifikationer med menneskelig vejledning, og anmeldere, der tester, om udsagnene fanger meningsfulde sikkerhedsegenskaber. Lean kontrollerer det resulterende bevis' logik. Mennesker forbliver ansvarlige for at vælge et stærkt mål, gennemgå antagelser og bedømme foreslåede ændringer til den godkendte specifikation.

### Hvorfor verificere kompileret maskinkode i stedet for at stole på Rust-kompileren?

Et bevis om den kompilerede binær etablerer direkte de angivne egenskaber for den artefakt. Google DeepMinds papir forklarer, at en kompileringsfejl, der overtræder en af disse egenskaber, ville gøre teoremet falsk. Rust-kompileren forlader derfor den betroede base for denne påstand. Beviset stoler stadig på instruktionsmodellen, Leans kerne og specificerede kryptografiske kontrakter.

### Hvordan forhindrer komparatoren en bevisagent i at svække sit mål?

Komparatoren kontrollerer teoremet og enhver definition, det afhænger af, mod en beskyttet godkendt specifikation. Google DeepMinds papir siger, at bevisagenter ikke kan skrive til den tilbageholdte kopi. Kontrollen kontrollerer også tilladte aksiomer og afspiller beviset i en frisk kerne. Foreslåede specifikationsændringer følger en separat gennemgået proces, mens mennesker forbliver ansvarlige for målets styrke.

### Hvad var The Daily Diff's dom over arbejdsgangen med kontrollerede beviser?

The Daily Diffs dom var SHIP IT. Niko ville implementere arbejdsgangen med kontrollerede beviser, fordi den godkendte påstand forbliver adskilt fra agenten, der producerer svaret. Han ville holde omfanget og antagelserne knyttet til hvert resultat. Episoden rapporterer Googles offentliggjorte bevisartefakt uden uafhængigt at genopbygge det og godkender arbejdsgangen inden for disse bevisgrænser.

## Kapitler

- 0:00 Hvem kontrollerer et AI-sikkerhedsbevis?
- 0:57 Hvordan bliver en påstand et bevisobjekt?
- 1:39 Hvorfor bevise den kompilerede binær?
- 2:16 Hvilke sikkerhedsegenskaber overlevede implementeringsgabet?
- 2:59 Kan specifikationen afvise ødelagt kode?
- 3:36 Kan et korrekt bevis besvare det forkerte spørgsmål?
- 4:13 Hvad fanger de skiftende målposter?
- 4:53 Ville jeg implementere denne bevisarbejdsgang?

## Oversat udskrift

Oversat fra den originale engelske fortælling. Tilgængelig lyd og undertekster styres af YouTube.

### Hvem kontrollerer et AI-sikkerhedsbevis?

0:00 En AI-sikkerhedsrevision lyder stadig som at stole på en chatbot. Googles nye Signal-resultat kommer med matematiske beviser, en separat kerne kontrollerer. Hvad beviste Google i denne video? Og hvordan forhindrer de en agent i at flytte målstolperne? Her er det nyttige svar. Modeller skriver kandidatbeviser, og Lean kontrollerer beviserne mod en menneskegodkendt påstand om udvalgt kompileret kode. Mennesker ejer stadig påstanden og antagelserne.

0:21 Du kan kontrollere resultatet uden at tro på modellens sejrstale. Et separat tjek fanger stille ændring af spørgsmålet. Vi vil følge det ned til definitionerne. Det er tirsdag den ti. november, og dette er The Daily Diff. AlphaProof Code er Googles ramme for at skrive software-specifikationer med menneskelig vejledning og generere kontrollerede beviser med AI-agenter. Denne undersøgelse retter sig mod libsignal, Rust-biblioteket, der implementerer Signals meddelelsesprotokol, inde i et bestemt kommandolinjeprogram.

0:45 Google annoncerede arbejdet i dag. Deres papir siger, at fem forskere arbejdede i fire uger. Agenter skrev beviserne, mens mennesker brugte det meste af deres indsats på specifikationerne. Krav har fundet en måde at blive endnu dyrere møder. Specifikationen angiver, hvad programmet skal gøre,

### Hvordan bliver en påstand et bevisobjekt?

0:59 hvad en angriber kontrollerer, og hvilke antagelser argumentet kræver. Anmeldere spørger, om det fanger den sikkerhed, folk bekymrer sig om. Et smukt kontrolleret svar på et svagt spørgsmål lader spørgsmålet være intakt. Teamet bygger på tidligere forskning i Signals handshake og dets meddelelsesnøgle-"ratchet". Formelle analyser havde allerede studeret disse designs. Googles påstand forbinder deres sikkerhedsargumenter med en umodificeret produktionsbiblioteks kompilerede implementering, hvor designet skal overleve kontakt med faktisk kode. Signals teknologichef, Ehren Kret,

1:27 beskriver en udvidelse ud over tidligere verifikations mindre omfang. Implementeringsdetaljer inkluderer meddelelser uden for rækkefølge og arkiverede sessioner for forsinkede meddelelser. Rigtig software gemmer de kvitteringer, dit elegante diagram smed væk. Forskerne kompilerer det umodificerede Rust-bibliotek med standardkompileren

### Hvorfor bevise den kompilerede binær?

1:41 til en Arm 64-bit Linux-udførelsesfil. Deres teoremer beskriver det binære ved hjælp af en formel instruktionsmodel, der strækker sig over gabet mellem kildekode og optimeret maskinkode. En kompileringsfejl, der bryder en angivet egenskab, ville gøre dens teorem falsk. Kompileren forlader derfor den betroede base for denne binærfil. Du stoler stadig på instruktionsmodellen og Leans checker. Tillidsgrænsen flyttede sig, og den har en adresse. Omkring seks og en halv million linjer kontrolleret bevis hviler på cirka seksogtyve

2:06 tusind betroede specifikations- og instruktionssemantiklinjer. Disse er artefaktantal. At behandle dem som intelligensscore er som at rangere udviklere efter størrelsen af deres node\_modules-mappe.

### Hvilke sikkerhedsegenskaber overlevede implementeringsgabet?

2:16 Argumenterne dækker meddelelsesfortrolighed og -autentifikation, med forward secrecy og post-kompromitteringssikkerhed under angivne modeller. De sidste to beskriver grænser for skade fra stjålne nøgler og genopretning efter friske udvekslinger. Hver garanti har betingelser for angriberen og sessionen. Kryptografiske primitiver ligger bag betroede kontrakter. Beviset antager, at disse rutiner opfører sig som specificeret og bygger på kryptografiske sikkerhedsantagelser. Et bevis idealiserer kryptografi; det andet ræsonnerer om angriberens succes sandsynligheder.

2:42 Begge har begrænsninger for de scenarier, de dækker. Spørg hvilken build, hvilken egenskab og hvilke antagelser. Dette resultat vedrører forskernes kommandolinje-harness. Gruppebeskeder er fremtidigt arbejde, og den beregningsmæssige model udelukker flerenhedstilstand. At kalde enhver Signal-installation fejlfri er uden for teoremet. Forskerne genindførte to tidligere rettede Signal-fejl i

### Kan specifikationen afvise ødelagt kode?

3:02 isolerede kopier og kompilerede dem. Kontrollerede beviser viste, at disse binærfiler overtrådte det symbolske sikkerhedsteorem. Det testede, om specifikationen kunne afvise reelle, ødelagte implementeringer. Dit grønne flueben har brug for en rød test. Google udgiver specifikationer og beviser med kontrolinstruktioner. Repositoryet siger, at en ren build tager timer og betydelig hukommelse. At læse annonceringen er betydeligt lettere på laptoppen. Hardwaremodellen og betroede kontrakter skal stadig gennemgås.

3:26 Jeg har ikke genopbygget den enorme artefakt til denne episode. Vi rapporterer det offentliggjorte resultat og dets grænser. Udenforstående har en vej til at inspicere det, hvilket betyder mere for mig end endnu en AI sejrsrunde. Nu fælden.

### Kan et korrekt bevis besvare det forkerte spørgsmål?

3:36 Lean kan acceptere et korrekt bevis for en udsagn, der næsten intet spørger om. Umulige antagelser kan gøre et teorem tomt. At ændre en definition begravet under overskriftens teorem kan svække målet. Artiklen designer kontroller mod dette. Portvogteren opretholder en tilbageholdt godkendt specifikation, som bevisagenter ikke kan skrive til. De kan foreslå korrektioner gennem en separat ændringsproces. Sikkerhedsforringelse eskalerer som en potentiel fejl. Beviserens erklæring om succes har ingen autoritet her.

4:00 Mennesker bedømmer ændringer i betroede antagelser, direkte eller gennem deres politik, og gennemgår ændringer efter hver kampagne. Ekspertvurdering forbliver ansvarlig. Agenten kan anmode om en anden opgave. Den kan ikke give sig selv en bestået karakter.

### Hvad fanger de skiftende målposter?

4:13 Her er det lovede tjek. Leans komparator sammenligner teoremet og hver definition, det afhænger af, med den beskyttede godkendte kopi. Den kontrollerer også tilladte aksiomer og afspiller beviset i en frisk kerne. Stille svækkelse af en hjælpedefinition ændrer derfor det, der sammenlignes. Et accepteret bevis skal etablere det godkendte mål. Det overlader stadig mennesker ansvaret for at vælge et stærkt mål og ærlige antagelser. For din egen AI-arbejdsgang skal du holde acceptkriterierne uden for

4:37 medarbejderens redigeringstilladelser og gennemgå foreslåede ændringer separat. Googles resultat gør den adskillelse konkret. Bevisskriveren udfører arbejdet; kontrolgrænsen afgør, om det tæller. Hvis du hellere vil læse dette end høre mig sige det, lander diff'en i din indbakke hver morgen, gratis på thedailydiff.dev, link nedenfor. Så dagens dom er SHIP IT.

### Ville jeg implementere denne bevisarbejdsgang?

4:54 Jeg ville implementere denne kontrollerede bevis-arbejdsgang, fordi den godkendte påstand forbliver adskilt fra agenten, der producerer svaret. Jeg ville holde omfanget og antagelserne knyttet til hvert resultat. Abonner, tryk på klokken, og fortæl mig i kommentarerne, om du ville have stemplet det anderledes. Og det er dagens diff. Jeg er Niko fra Axrisi. Fusioner ansvarligt.

## Kilder

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub