# AlphaProof Code and Signal: provjereni sigurnosni dokazi strojnog koda i povjerljive pretpostavke

Published: 2026-11-11

Google DeepMind izvještava o strojno provjerenim dokazima odabranih sigurnosnih svojstava za kompiliranu libsignal komandno-linijsku implementaciju. Lean provjerava dokaz, dok ljudi odobravaju specifikaciju i njezine pretpostavke. Zasebni uspoređivač provjerava teorem i sve ovisne definicije u odnosu na odobrenu ciljnu specifikaciju.

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

## Što ovaj video pokriva

- AI agenti proizvode kandidatne dokaze; Leanova jezgra provjerava uspostavljaju li oni ljudski odobrenu formalnu tvrdnju.
- Provjereni cilj je određena kompiliranana libsignal CLI implementacija, s pouzdanom semantikom i kriptografskim ugovorima.
- Dokazivanje kompiliranog binarnog koda uklanja Rust kompajler iz pouzdane baze za navedena svojstva tog binarnog koda.
- Istraživači izvještavaju o dva izolirana ponovna uvođenja prethodno ispravljenih bugova koji krše njihov simbolički sigurnosni teorem.
- Uspoređivač provjerava teorem i svaku ovisnu definiciju u odnosu na zaštićenu odobrenu specifikaciju; izmjene prolaze kroz zaseban postupak pregleda.

## Pitanja i odgovori

### Što je AlphaProof Code dokazao o Signalovoj implementaciji?

Google DeepMind izvještava o provjerenim dokazima odabranih sigurnosnih svojstava za kompiliranu libsignal komandno-linijsku implementaciju. Tehnički rad pokriva povjerljivost i autentičnost poruka, s povratnom tajnošću i sigurnošću nakon kompromitacije prema navedenim modelima. Rezultat zadržava uvjete o napadaču, sesiji i kriptografskim pretpostavkama. Njegov opseg isključuje opće jamstvo za svaku Signal aplikaciju ili instalaciju.

### Tko odlučuje što AI-generirani sigurnosni dokaz mora uspostaviti?

Ljudski recenzenti odobravaju specifikaciju i njezine pretpostavke. Tehnički rad Google DeepMinda opisuje agente koji izrađuju specifikacije uz ljudsko vodstvo i recenzente koji testiraju obuhvaćaju li izjave značajna sigurnosna svojstva. Lean provjerava logiku rezultirajućeg dokaza. Ljudi ostaju odgovorni za odabir jakog cilja, pregled pretpostavki i prosuđivanje predloženih promjena odobrene specifikacije.

### Zašto verificirati kompiliran strojni kod umjesto povjerenja u Rust kompajler?

Dokaz o kompiliranom binarnom kodu izravno uspostavlja navedena svojstva za taj artefakt. Rad Google DeepMinda objašnjava da bi greška kompajlera koja krši jedno od tih svojstava učinila teorem lažnim. Rust kompajler stoga napušta pouzdanu bazu za ovu tvrdnju. Dokaz još uvijek vjeruje u model instrukcija, Leanovu jezgru i navedene kriptografske ugovore.

### Kako uspoređivač sprječava agenta za dokazivanje da oslabi svoj cilj?

Uspoređivač provjerava teorem i svaku definiciju o kojoj ovisi u odnosu na zaštićenu odobrenu specifikaciju. Rad Google DeepMinda kaže da agenti za dokazivanje ne mogu pisati u tu zaštićenu kopiju. Provjeravač također provjerava dopuštene aksiome i ponovno reproducira dokaz u novoj jezgri. Predložene izmjene specifikacije slijede zaseban postupak pregleda, dok ljudi ostaju odgovorni za snagu cilja.

### Kakva je bila presuda The Daily Diffa o tijeku rada s provjerenim dokazima?

Presuda The Daily Diffa bila je SHIP IT. Niko bi isporučio tijek rada s provjerenim dokazima jer odobrena tvrdnja ostaje odvojena od agenta koji proizvodi odgovor. Zadržao bi opseg i pretpostavke priložene svakom rezultatu. Epizoda izvještava o Googleovom objavljenom dokaznom artefaktu bez neovisne ponovne izgradnje i odobrava tijek rada unutar tih granica dokaza.

## Poglavlja

- 0:00 Tko provjerava AI sigurnosni dokaz?
- 0:57 Kako tvrdnja postaje cilj dokazivanja?
- 1:39 Zašto dokazati kompiliranu binarnu datoteku?
- 2:16 Koja su sigurnosna svojstva preživjela jaz u implementaciji?
- 2:59 Može li specifikacija odbiti neispravan kod?
- 3:36 Može li ispravan dokaz odgovoriti na pogrešno pitanje?
- 4:13 Što hvata pokretne ciljeve?
- 4:53 Bih li isporučio ovaj tijek rada s dokazima?

## Prevedeni transkript

Prevedeno iz izvornog engleskog pripovijedanja. Dostupni zvuk i titlovi kontroliraju se putem YouTubea.

### Tko provjerava AI sigurnosni dokaz?

0:00 Sigurnosna revizija AI-ja i dalje zvuči kao povjerenje chatbotu. Googleov novi Signal rezultat dolazi s matematičkim dokazima koje provjerava zasebna jezgra. U ovom videu, što je Google dokazao? I kako sprječavaju agenta da mijenja pravila igre? Evo korisnog odgovora. Modeli pišu kandidatne dokaze, a Lean provjerava dokaze u odnosu na tvrdnju koju je odobrio čovjek o odabranom kompiliranom kodu. Ljudi i dalje posjeduju tvrdnju i pretpostavke.

0:21 Rezultat možete provjeriti bez vjerovanja u pobjednički govor modela. Zasebna provjera sprječava tiho mijenjanje pitanja. Pratit ćemo to do definicija. Utorak je, deseti studeni, a ovo je The Daily Diff. AlphaProof Code je Googleov okvir za pisanje softverskih specifikacija uz ljudsko vodstvo i generiranje provjerenih dokaza s AI agentima. Ova studija cilja libsignal, Rust biblioteku koja implementira Signalov protokol za razmjenu poruka, unutar određenog programa komandne linije.

0:45 Google je danas najavio rad. U radu stoji da je pet istraživača radilo preko četiri tjedna. Agenti su pisali dokaze, dok su ljudi većinu svog truda posvetili specifikacijama. Zahtjevi su pronašli način da postanu još skuplji sastanci. Specifikacija govori što program mora učiniti,

### Kako tvrdnja postaje cilj dokazivanja?

0:59 što napadač kontrolira i koje pretpostavke argument treba. Recenzenti pitaju obuhvaća li sigurnost o kojoj se ljudi brinu. Prekrasno provjeren odgovor na slabo pitanje ostavlja to pitanje netaknutim. Tim se nadovezuje na ranija istraživanja Signalovog rukovanja i njegovog ključa za poruke. Formalne analize već su proučavale te dizajne. Googleova tvrdnja povezuje njihove sigurnosne argumente s neizmijenjenom proizvodnom kompiliranom implementacijom biblioteke, gdje dizajn mora preživjeti kontakt sa stvarnim kodom. Signalov glavni tehnološki direktor, Ehren Kret,

1:27 opisuje proširenje izvan ranijih manjih opsega provjere. Detalji implementacije uključuju poruke izvan reda i arhivirane sesije za odgođene poruke. Stvarni softver čuva potvrde koje je vaš elegantan dijagram odbacio. Istraživači kompiliraju neizmijenjenu Rust biblioteku standardnim

### Zašto dokazati kompiliranu binarnu datoteku?

1:41 kompajlerom u izvršnu datoteku Arm 64 Linux. Njihovi teoremi opisuju tu binarnu datoteku koristeći formalni model instrukcija, premošćujući jaz između izvornog i optimiziranog strojnog koda. Greška kompajlera koja krši navedeno svojstvo učinila bi njegov teorem lažnim. Kompajler stoga napušta pouzdanu bazu za ovu binarnu datoteku. Još uvijek vjerujete u model instrukcija i Leanov provjeravač. Granica povjerenja se pomaknula i ima adresu. Oko šest i pol milijuna redaka provjerenog dokaza počiva na otprilike dvadeset i šest

2:06 tisuća pouzdanih redaka specifikacije i semantike instrukcija. To su brojevi artefakata. Tretiranje njih kao rezultata inteligencije je kao rangiranje programera po veličini njihove mape node modula.

### Koja su sigurnosna svojstva preživjela jaz u implementaciji?

2:16 Argumenti pokrivaju povjerljivost i autentičnost poruka, s povratnom tajnošću i sigurnošću nakon kompromitacije prema navedenim modelima. Ona posljednja dva opisuju ograničenja štete od ukradenih ključeva i oporavak nakon novih razmjena. Svako jamstvo ima uvjete o napadaču i sesiji. Kriptografski primitivi nalaze se iza pouzdanih ugovora. Dokaz pretpostavlja da se te rutine ponašaju kako je navedeno i oslanja se na kriptografske sigurnosne pretpostavke. Jedan dokaz idealizira kriptografiju; drugi rezonira o vjerojatnosti uspjeha napadača.

2:42 Oba imaju ograničenja na scenarije koje pokrivaju. Pitajte koju verziju, koje svojstvo i koje pretpostavke. Ovaj rezultat se odnosi na komandno-linijsku implementaciju istraživača. Grupne poruke su budući rad, a računski model isključuje stanje više uređaja. Tvrdnja da je svaka instalacija Signala bez grešaka izlazi izvan teorema. Istraživači su ponovno uveli dva prethodno ispravljena Signal buga u

### Može li specifikacija odbiti neispravan kod?

3:02 izolirane kopije i kompilirali ih. Provjereni dokazi pokazali su da te binarne datoteke krše simbolički sigurnosni teorem. Time je testirano može li specifikacija odbiti stvarne neispravne implementacije. Vaša zelena kvačica treba crveni test. Google objavljuje specifikacije i dokaze s uputama za provjeru. Spremnik kaže da čista izrada traje satima i zahtijeva značajnu memoriju. Čitanje objave znatno je lakše na prijenosnom računalu. Model hardvera i pouzdani ugovori još uvijek trebaju pregled.

3:26 Nisam ponovno izgradio ogroman artefakt za ovu epizodu. Izvještavamo o objavljenom rezultatu i njegovim granicama. Vanjski ljudi imaju put da ga pregledaju, što mi je važnije od još jednog AI kruga pobjede. Sada zamka.

### Može li ispravan dokaz odgovoriti na pogrešno pitanje?

3:36 Lean može prihvatiti ispravan dokaz tvrdnje koja ne traži gotovo ništa. Nemoguće pretpostavke mogu učiniti teorem praznim. Promjena definicije zakopane ispod naslovnog teorema može oslabiti cilj. Rad dizajnira provjere protiv toga. Vratar čuva zaštićenu odobrenu specifikaciju u koju agenti za dokazivanje ne mogu pisati. Oni mogu predložiti ispravke kroz zaseban postupak izmjena. Oslabljenje sigurnosti eskalira se kao potencijalni bug. Izjava dokazivača o uspjehu ovdje nema autoritet.

4:00 Ljudi prosuđuju promjene pouzdanih pretpostavki, izravno ili putem svoje politike, i pregledavaju izmjene nakon svake kampanje. Stručno mišljenje ostaje odgovorno. Agent može zatražiti drugačiji zadatak. Ne može si dati prolaznu ocjenu.

### Što hvata pokretne ciljeve?

4:13 Evo obećane provjere. Leanov uspoređivač uspoređuje teorem i svaku definiciju o kojoj ovisi s tom zaštićenom odobrenom kopijom. Također provjerava dopuštene aksiome i ponovno reproducira dokaz u novoj jezgri. Tiho slabljenje pomoćne definicije stoga mijenja ono što se uspoređuje. Prihvaćeni dokaz mora uspostaviti odobreni cilj. To još uvijek ostavlja ljude odgovornima za odabir jakog cilja i poštenih pretpostavki. Za vaš vlastiti AI radni proces, držite kriterije prihvaćanja izvan

4:37 dozvole za uređivanje radnika i odvojeno pregledajte predložene promjene. Googleov rezultat konkretizira to razdvajanje. Pisac dokaza obavlja posao; granica provjere odlučuje hoće li se to računati. Ako ovo radije čitate nego da me slušate, the diff vam stiže u inbox svako jutro, besplatno na daily diff dot dev, link ispod. Dakle, današnja presuda je SHIP IT.

### Bih li isporučio ovaj tijek rada s dokazima?

4:54 Poslao bih ovaj provjereni tijek rada dokazivanja jer odobrena tvrdnja ostaje odvojena od agenta koji proizvodi odgovor. Držao bih opseg i pretpostavke priložene svakom rezultatu. Pretplatite se, pritisnite zvono i recite mi u komentarima biste li ga označili drugačije. I to je diff za danas. Ja sam Niko iz Axrisija. Spajajte odgovorno.

## Izvori

- [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