# I-AlphaProof Code kanye neSiginali: ubufakazi bokuphepha kwekhodi yomshini ohloliwe kanye nezinto eziyizingqinamba ezithenjwayo

Published: 2026-11-11

I-Google DeepMind ibika ubufakazi obuhlolwe ngomshini bezakhi ezikhethiwe zokuphepha ze-libsignal command-line harness ehlanganisiwe. I-Lean ihlola ubufakazi, kanti abantu bavuma imininingwane kanye nezinto eziyizingqinamba zayo. Isiqhathanisi esihlukile sihlola i-theorem nazo zonke izincazelo eziyizinsika ngokuphambene nethagethi evunyiwe.

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

## Lokho okuhlanganiswa yile vidiyo

- Ama-ejenti e-AI akhiqiza ubufakazi obungaba khona; inhloko ye-Lean ihlola ukuthi ziwenza yini umuntu avunyelwe ukufaka isicelo.
- Ithagethi eqinisekisiwe iyi-libsignal CLI harness ehlanganisiwe ethile, enezincazelo ezithenjwayo kanye nezivumelwano ze-cryptographic.
- Ukufakazela i-binary ehlanganisiwe kususa i-Rust compiler kusisekelo esithenjwayo sezinto ezishiwo ze-binary.
- Abacwaningi babika izinto ezimbili ezihlukene zokuphinde kungenise izimbungulu ezazilungisiwe ngaphambilini ezishaya indiva i-symbolic security theorem yabo.
- Isiqhathanisi sihlola i-theorem nazo zonke izincazelo eziyizinsika ngokuphambene nemininingwane evunyiwe evikelekile; izichibiyelo zidlula inqubo ehlukile ebuyekezwe.

## Imibuzo nezimpendulo

### Yini i-AlphaProof Code eyifakazela mayelana nokusetshenziswa kwe-Signal?

I-Google DeepMind ibika ubufakazi obuhlolwe bezakhi ezikhethiwe zokuphepha ze-libsignal command-line harness ehlanganisiwe. Iphepha lobuchwepheshe lihlanganisa ukugcinwa kwemfihlo yemiyalezo nokuqinisekiswa, ngemfihlo ephambili kanye nokuphepha ngemuva kokungena ngaphansi kwamamodeli ashiwo. Umphumela ugcina izimo kumhlaseli, iseshini kanye nezinto eziyizingqinamba zokubethela. Ububanzi bawo abubandakanyi isiqinisekiso esiphelele sawo wonke uhlelo lwe-Signal noma ukufakwa.

### Ubani onquma ukuthi ubufakazi bokuphepha obukhiqizwe yi-AI kufanele bubuqinisekise ngani?

Ababuyekezi abangabantu bavumela imininingwane kanye nezinto eziyizingqinamba zayo. Iphepha lobuchwepheshe le-Google DeepMind lichaza ama-ejenti adala imininingwane ngosizo lwabantu kanye nababuyekezi behlola ukuthi izitatimende zizibamba yini izakhi zokuphepha ezibalulekile. I-Lean ihlola ingqondo yobufakazi obubangelwayo. Abantu basanesibopho sokukhetha ithagethi eqinile, ukubuyekeza izinto eziyizingqinamba kanye nokwahlulela izinguquko eziphakanyisiwe kumininingwane evunyiwe.

### Kungani kufanele kuqinisekiswe ikhodi yomshini ehlanganisiwe esikhundleni sokuthembela ku-Rust compiler?

Ubufakazi obumayelana ne-binary ehlanganisiwe buqinisekisa izakhi ezishiwo zale artifact ngqo. Iphepha le-Google DeepMind lichaza ukuthi iphutha le-compiler eliphula esinye salezo zakhi lingenze i-theorem ingamanga. Ngakho-ke i-Rust compiler ishiya isisekelo esithenjwayo saleli cala. Ubufakazi busathemba imodeli yemiyalo, inhloko ye-Lean kanye nezivumelwano ezibekiwe zokubethela.

### Isiqhathanisi siyimisa kanjani i-ejenti yobufakazi ukuthi ingabuthakathisi ithagethi yayo?

Isiqhathanisi sihlola i-theorem nazo zonke izincazelo ezithembela kuyo ngokuphambene nemininingwane evunyiwe evikelekile. Iphepha le-Google DeepMind lithi ama-ejenti abufakazi angenakuyibhala leyo khophi egciniwe. Isihloli sihlola futhi ama-axiom avunyelwe futhi sidlale kabusha ubufakazi engqikithini entsha. Izichibiyelo zemininingwane eziphakanyisiwe zilandela inqubo ehlukile ebuyekezwe, kanti abantu basanesibopho sokuba namandla ethagethi.

### Siyini isinqumo seThe Daily Diff ngomsebenzi wobufakazi obuhlolwe?

Isinqumo seThe Daily Diff kwaba yi-SHIP IT. UNiko ubengawuthatha lo msebenzi wobufakazi obuhlolwe ngoba isicelo esivunyiwe sihlala sihlukile ku-agent ekhiqiza impendulo. Ubengawugcina ububanzi kanye nezinto eziyizingqinamba ezihambisana nawo wonke umphumela. Lesi siqephu sibika i-artifact yobufakazi eshicilelwe yeGoogle ngaphandle kokuyakha kabusha ngokuzimela futhi sivumela umsebenzi ngaphakathi kwemingcele yalobo bufakazi.

## Izahluko

- 0:00 Ubani ohlola ubufakazi bokuphepha be-AI?
- 0:57 Siba kanjani isicelo ithagethi yobufakazi?
- 1:39 Kungani kufanele kufakazelwe i-binary ehlanganisiwe?
- 2:16 Yiziphi izakhi zokuphepha ezasinda ekushiyweni kokusetshenziswa?
- 2:59 Ingabe imininingwane ingayenqaba ikhodi ephukile?
- 3:36 Ingabe ubufakazi obulungile bungaphendula umbuzo ongalungile?
- 4:13 Yini ebamba izinhloso ezihambayo?
- 4:53 Ngingawuthatha yini lo msebenzi wobufakazi?

## Umbhalo obhaliwe ohunyushwe

Kuhunyushwe kusuka ekulandiseni kokuqala kwesiNgisi. Umsindo namazwibela atholakalayo alawulwa yi-YouTube.

### Ubani ohlola ubufakazi bokuphepha be-AI?

0:00 Ukucwaninga okuphepha kwe-AI kusazwakala njengokuthembela ku-chatbot. Umphumela omusha we-Signal kaGoogle uza nobufakazi bezibalo nengqikithi ehlukile ihlola. Kule vidiyo, yini eyayifakazelwa yiGoogle? Futhi bayimisa kanjani i-agent ukuthi ihambise izinhloso? Nansi impendulo ewusizo. Amamodeli abhala ubufakazi obungaba khona, futhi i-Lean ihlola ubufakazi ngokuphambene nesicelo esivunyelwe ngabantu mayelana nekhodi ehlanganisiwe ekhethiwe. Abantu basenezicelo kanye nezinto eziyizingqinamba.

0:21 Ungawuhlola umphumela ngaphandle kokukholwa inkulumo yokunqoba yemodeli. Ukuhlolwa okuhlukile kubamba ukushintsha umbuzo buthule. Sizokulandela kuze kube yizincazelo. NgoLwesibili, Novemba leshumi, futhi lokhu The Daily Diff. I-AlphaProof Code iwuhlaka lweGoogle lokubhala imininingwane yesofthiwe ngosizo lwabantu futhi ikhiqiza ubufakazi obuhlolwe ngama-ejenti e-AI. Lolu cwaningo lugxile ku-libsignal, umtapo wezincwadi we-Rust osebenzisa iphrothokholi yokuthumela imiyalezo ye-Signal, ngaphakathi kohlelo oluthile lomugqa wokulayisha.

0:45 IGoogle ikhuthaze umsebenzi namuhla. Iphepha layo lithi abacwaningi abahlanu basebenze isikhathi esingaphezu kwamaviki amane. Ama-ejenti abhala ubufakazi, kanti abantu bachithe iningi lomzamo wabo ekunqumeni imininingwane. Izidingo zithole indlela yokuba imihlangano ebiza kakhulu. Imininingwane ithi uhlelo kufanele lwenzani,

### Siba kanjani isicelo ithagethi yobufakazi?

0:59 yini umhlaseli ayilawulayo, nokuthi yiziphi izinto eziyizingqinamba ezidingwa yimpikiswano. Ababuyekezi babuza ukuthi iyazibamba yini izinto zokuphepha abantu abazikhathalelayo. Impendulo ehlolwe kahle kakhulu embuzweni obuthaka ishiya lowo mbuzo unjalo. Ithimba lakha phezu kocwaningo olwedlule mayelana nokuphathana kwe-Signal kanye ne-message-key ratchet yayo. Ukuhlaziya okusemthethweni kwasevele kwafunda leyo midwebo. Isicelo seGoogle sixhuma izimangalo zabo zokuphepha ekuqalisweni okuhlanganisiwe komtapo wezincwadi wokukhiqiza ongalungisiwe, lapho umdwebo kufanele usinde ukuhlangana nekhodi yangempela. Umphathi wezobuchwepheshe be-Signal, u-Ehren Kret,

1:27 uchaza ukwanda ngaphezu kobubanzi obuncane bokuqinisekisa kwangaphambilini. Imininingwane yokusebenzisa ihlanganisa imiyalezo engekho endaweni kanye nezikhathi ezilondoloziwe zemiyalezo ebuye yakulazwa. Isofthiwe yangempela igcina amaresidi isichathulelo sakho esihle esilahle kude. Abacwaningi bahlanganisa umtapo wezincwadi we-Rust ongalungisiwe nge-compiler ejwayelekile

### Kungani kufanele kufakazelwe i-binary ehlanganisiwe?

1:41 ibe yi-Arm sixty-four Linux executable. Ama-theorem abo achaza leyo binary besebenzisa imodeli yemiyalo esemthethweni, efinyelela ngaphesheya kwephutha phakathi komthombo nekhodi yomshini elungiselelwe. Iphutha le-compiler eliphula isici esishiwo lingenze i-theorem yalo ingamanga. Ngakho-ke i-compiler ishiya isisekelo esithenjwayo sale binary. Usayethemba imodeli yemiyalo kanye ne-checker ye-Lean. Umngcele wokuthembeka ususukile, futhi unekheli. Cishe izigidi eziyisithupha nezinhlamvu eziyizinkulungwane ezingamakhulu amahlanu zobufakazi obuhlolwe zisekelwe kumigqa

2:06 eyiminyaka engaba izinkulungwane ezingamashumi amabili nesithupha yemininingwane ethenjwayo kanye nemiyalo. Lezi izibalo zama-artifact. Ukuziphatha njengezibalo zobuhlakani kufana nokulinganisa abathuthukisi ngobukhulu befolda yabo yama-node modules.

### Yiziphi izakhi zokuphepha ezasinda ekushiyweni kokusetshenziswa?

2:16 Izimangalo zihlanganisa ukugcinwa kwemfihlo yemiyalezo kanye nokuqinisekisa, ngemfihlo ephambili kanye nokuphepha ngemuva kokungena ngaphansi kwamamodeli ashiwo. Lezi ezimbili zokugcina zichaza imingcele emonakalweni wezitshalo ezebiwe nokubuyiselwa ngemuva kokushintshana okusha. Isiqinisekiso ngasinye sinezimo kumhlaseli naseshashaneni. Izinhlelo zokubethela zihlala ngemuva kwezivumelwano ezithenjwayo. Ubufakazi bucabanga ukuthi lezi zinqubo zisebenza njengoba zichazwe futhi zithembela ezintweni eziyizingqinamba zokuphepha kwezokubethela. Olunye ubufakazi lucabanga nge-cryptography; okunye lufaka amathuba okuphumelela komhlaseli.

2:42 Zombili zinezingqinamba ezimweni ezizihlanganisayo. Buza ukuthi iyiphi i-build, iyiphi isici, nokuthi yiziphi izinto eziyizingqinamba. Lo mphumela uphathelene ne-command-line harness yabacwaningi. Ukuthumela imiyalezo yeqembu kungumsebenzi wesikhathi esizayo, futhi imodeli yokubala ayibandakanyi isimo samadivayisi amaningi. Ukubiza konke ukufakwa kwe-Signal kungena embungwini kuphumela ngaphandle kwe-theorem. Abacwaningi baphinde bangenisa izimbungulu ezimbili ze-Signal ezazilungisiwe ngaphambilini

### Ingabe imininingwane ingayenqaba ikhodi ephukile?

3:02 ezakopishwa futhi bazihlanganisa. Ubufakazi obuhlolwe babonisa ukuthi lezo binaries zaziphula i-symbolic security theorem. Lokho kwahlola ukuthi imininingwane ingakwazi yini ukwenqaba izinhlelo ezisebenzayo eziphukile. Uphawu lwakho oluluhlaza ludinga ukuhlolwa okubomvu. IGoogle ishicilela imininingwane nobufakazi ngemiyalelo yokuhlola. I-repository ithi i-build ehlanzekile ithatha amahora nememori enkulu. Ukufunda isimemezelo kulula kakhulu ku-laptop. Imodeli yehadiwe kanye nezivumelwano ezithenjwayo kusadinga ukubuyekezwa.

3:26 Angikaze ngiyakhe kabusha i-artifact enkulu kulesi siqephu. Sibika umphumela oshicilelwe kanye nemingcele yawo. Abangaphandle banendlela yokuyihlola, okubaluleke kakhulu kimi kunokunye ukunqoba kwe-AI okukhulu. Manje isicupho.

### Ingabe ubufakazi obulungile bungaphendula umbuzo ongalungile?

3:36 I-Lean ingamukela ubufakazi obulungile besitatimende esicela cishe lutho. Izinto eziyizingqinamba ezingenzeki zingenza i-theorem ingenamsebenzi. Ukushintsha incazelo engcwatshiwe ngaphansi kwe-headline theorem kungabuthakathisa inhloso. Iphepha lidala ukuhlola ngokuphambene nalokhu. Umqaphi ugcina imininingwane evunyiwe evikelekile ama-ejenti abufakazi angenakuyibhala. Banga phakamisa izilungiso ngohlelo oluhlukile lokuchibiyela. Ukubuthakathiswa kwezokuphepha kuyakhuphulwa njengembungulu engaba khona. Isimemezelo somfakazeli sokuphumelela asinaso isiphathimandla lapha.

4:00 Abantu bahlulela izinguquko kuzinto eziyizingqinamba ezithenjwayo, ngqo noma ngenqubomgomo yabo, futhi babuyekeze izichibiyelo ngemuva komkhankaso ngamunye. Ukwahlulela kochwepheshe kusahlala kulukhuni. I-agent ingacela umsebenzi ohlukile. Ayikwazi ukuzinika ibanga lokuphasa.

### Yini ebamba izinhloso ezihambayo?

4:13 Nansi ukuhlola okuthenjisiwe. Isiqhathanisi se-Lean siqhathanisa i-theorem nazo zonke izincazelo ezithembela kuyo nekhophi evunyiwe evikelekile. Ihlola futhi ama-axiom avunyelwe futhi idlala kabusha ubufakazi engqikithini entsha. Ukubuthakathisa buthule incazelo yesisizi ngakho-ke kushintsha into eqhathaniswa. Ubufakazi obamukelwe kufanele buvumele ithagethi evunyiwe. Lokho kusashiya abantu benesibopho sokukhetha ithagethi eqinile kanye nezinto eziyizingqinamba eziqotho. Ngomsebenzi wakho we-AI, gcina imibandela yokwamukela ngaphandle kwezimvume zokuhlela

4:37 zomsebenzi futhi ubuyekeze izinguquko eziphakanyisiwe ngokwehlukana. Umphumela weGoogle wenza leyo nhlukaniso ibonakale. Umbhali wobufakazi wenza umsebenzi; umngcele wokuhlola unquma ukuthi uyabaluleka yini. Uma ungathanda ukufunda lokhu kunokuzwa ngikushoyo, i-diff ifika ebhokisini lakho le-imeyili njalo ekuseni, mahhala ku-the daily diff dot dev, isixhumanisi esingezansi. Ngakho isinqumo sanamuhla yi-SHIP IT.

### Ngingawuthatha yini lo msebenzi wobufakazi?

4:54 Ngingawuthatha lo msebenzi wobufakazi ohloliwe ngoba isicelo esivunyiwe sihlala sihlukile ku-agent ekhiqiza impendulo. Ngingawugcina ububanzi kanye nezinto eziyizingqinamba ezihambisana nawo wonke umphumela. Bhalisa, shaya insimbi, futhi ungitshele kumazwana uma ubungawubeka uphawu ngokwehlukile. Futhi yilokho okuhlukile kwanamuhla. NginguNiko ovela ku-Axrisi. Hlanganisa ngokukhalipha.

## Imithombo

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