# AlphaProof Code 與 Signal：已驗證機器碼安全證明與信任假設

Published: 2026-11-11

Google DeepMind 報告稱，針對編譯後的 libsignal 命令列程式，已完成選定安全屬性的機器驗證證明。Lean 檢查證明，而人類批准規範及其假設。一個獨立的比較器會根據經批准的目標檢查定理和所有相關定義。

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

## 本影片重點

- AI 代理生成候選證明；Lean 的核心檢查它們是否確立了人類批准的正式聲明。
- 驗證的目標是特定的編譯後的 libsignal CLI 程式，具有受信任的語義和加密合約。
- 證明編譯後的二進位文件，將 Rust 編譯器從該二進位文件指定屬性的信任基礎中移除。
- 研究人員報告了兩次獨立地重新引入先前修復的錯誤，這些錯誤違反了他們的符號安全定理。
- 比較器會根據受保護的批准規範檢查定理和每個相關定義；修訂版會通過單獨的審查流程。

## 問題與解答

### AlphaProof Code 證明了 Signal 實作的哪些內容？

Google DeepMind 報告稱，針對編譯後的 libsignal 命令列程式，已完成選定安全屬性的驗證證明。技術論文涵蓋訊息機密性和認證，在指定模型下具有前向保密和妥協後安全性。結果保留了對攻擊者、會話和密碼假設的條件。其範圍不包括對每個 Signal 應用程式或安裝的全面保證。

### 誰決定 AI 生成的安全證明必須確立什麼？

人類審閱者批准規範及其假設。Google DeepMind 的技術論文描述了代理在人類指導下起草規範，以及審閱者測試陳述是否捕捉到有意義的安全屬性。Lean 檢查生成的證明的邏輯。人類仍然負責選擇一個強大的目標、審閱假設並裁決對批准規範提出的更改。

### 為何驗證編譯後的機器碼而不是信任 Rust 編譯器？

關於編譯後的二進位文件的證明直接確立了該成品的指定屬性。Google DeepMind 的論文解釋說，違反其中一個屬性的編譯器錯誤會使定理為假。因此，Rust 編譯器脫離了此聲明的信任基礎。該證明仍然信任指令模型、Lean 的核心和指定的密碼學合約。

### 比較器如何阻止證明代理削弱其目標？

比較器會根據受保護的批准規範檢查定理及其所依賴的每個定義。Google DeepMind 的論文指出，證明代理無法寫入該保留副本。檢查器還會檢查允許的公理並在一個新的核心中重播證明。提議的規範修訂遵循單獨的審查流程，而人類仍然負責目標的強度。

### The Daily Diff 對已驗證的證明工作流程的判斷是什麼？

The Daily Diff 的判斷是 SHIP IT。Niko 會發布已驗證的證明工作流程，因為經批准的聲明與生成答案的代理保持分離。他會將範圍和假設附加到每個結果。該集報告了 Google 已發布的證明成品，但未獨立重建它，並在這些證據範圍內批准了該工作流程。

## 章節

- 0:00 誰來檢查 AI 安全證明？
- 0:57 聲明如何成為證明目標？
- 1:39 為何證明已編譯的二進位文件？
- 2:16 哪些安全屬性經受住了實施差距？
- 2:59 規範能拒絕破損的程式碼嗎？
- 3:36 正確的證明會回答錯誤的問題嗎？
- 4:13 什麼捕捉了移動的目標？
- 4:53 我會發布這個證明工作流程嗎？

## 翻譯文字稿

譯自英文原版旁白。可用的音訊和字幕由 YouTube 控制。

### 誰來檢查 AI 安全證明？

0:00 AI 安全審計聽起來仍然像信任一個聊天機器人。 Google 的新 Signal 結果附帶一個獨立核心的數學證明 檢查。在這個影片中，Google 證明了什麼？ 他們如何阻止代理移動目標？ 這是一個有用的答案。 模型撰寫候選證明，而 Lean 根據 人類批准的關於選定編譯程式碼的聲明檢查證明。 人類仍然擁有聲明和假設。

0:21 您可以檢查結果，而不必相信模型的勝利演講。 單獨的檢查會發現悄悄改變問題的行為。 我們將追溯到定義。 今天是十一月十日星期二，這是 The Daily Diff。 AlphaProof Code 是 Google 的框架，用於在 人類指導下撰寫軟體規範，並使用 AI 代理生成已驗證的證明。 這項研究的目標是 libsignal，即在特定命令列程式中實作 Signal 訊息協定的 Rust 函式庫。 這項研究的目標是 libsignal，即在特定命令列程式中實作 Signal 訊息協定的 Rust 函式庫。

0:45 Google 今天宣布了這項工作。 其論文稱，五位研究人員工作了四週。 代理撰寫證明，而人類將大部分精力花在 規範上。需求已經找到了變得更昂貴的方法 會議。規範說明了程式必須做什麼，

### 聲明如何成為證明目標？

0:59 攻擊者控制什麼，以及論證需要哪些假設。 審查人員會詢問它是否捕捉到人們關心的安全性。 一個對弱問題進行了完美檢查的答案，仍然會讓該問題保持不變。 該團隊基於早期對 Signal 握手及其訊息金鑰 棘輪的研究。正式分析已經研究了這些設計。 Google 的聲明將他們的安全論證與未修改的生產 函式庫的編譯實作連接起來，其中設計必須經受住與 實際程式碼的接觸。Signal 的技術長 Ehren Kret

1:27 描述了超越早期驗證較小範圍的擴展。 實作細節包括亂序 訊息和歸檔會話以用於 延遲訊息。實際軟體會保留您優雅圖表丟棄的收據。 研究人員使用標準編譯器將未修改的 Rust 函式庫編譯成

### 為何證明已編譯的二進位文件？

1:41 Arm 64 位元 Linux 可執行檔。 他們的定理使用形式化的指令模型描述了該二進位文件， 跨越了原始碼和最佳化機器碼之間的差距。 破壞指定屬性的編譯器錯誤會使其定理為假。 因此，編譯器離開了此二進位文件的信任基礎。 您仍然信任指令模型和 Lean 的檢查器。 信任邊界已移動，並且它有一個地址。 大約六百五十萬行的已驗證證明，基於大約二萬六千行的

2:06 受信任規範和指令語義行。 這些是成品計數。 將它們視為智慧分數，就像根據節點模組資料夾的大小對開發人員進行排名一樣。 將它們視為智慧分數，就像根據節點模組資料夾的大小對開發人員進行排名一樣。

### 哪些安全屬性經受住了實施差距？

2:16 這些論證涵蓋訊息機密性和認證， 在指定模型下具有前向保密和後妥協安全性。 最後兩者描述了被盜金鑰損害的限制以及新 交換後的恢復。每個保證都對攻擊者和會話有條件。 密碼原語在受信任合約之後。 該證明假設這些常式按規定運行，並依賴於密碼學 安全假設。一個證明將密碼學理想化；另一個則推理 攻擊者成功的機率。

2:42 兩者都對其涵蓋的場景有限制。 詢問哪個建構、哪個屬性以及哪個假設。 此結果與研究人員的命令列工具相關。 群組訊息是未來的研究工作，計算模型排除了 多裝置狀態。稱每個 Signal 安裝都無錯誤，這超出了 定理的範圍。研究人員將兩個先前已修復的 Signal 錯誤重新引入

### 規範能拒絕破損的程式碼嗎？

3:02 獨立副本中並進行編譯。 經檢查的證明顯示這些二進位文件違反了符號安全定理。 這測試了規範是否能拒絕實際的損壞實作。 您的綠色勾選標記需要紅色測試。 Google 發布了規範和證明，並附有檢查說明。 儲存庫表示，一次乾淨的建構需要數小時和大量的記憶體。 在筆記型電腦上閱讀公告要容易得多。 硬體模型和受信任的合約仍然需要審查。

3:26 我尚未重建本集的大量成品。 我們正在報告已發表的結果及其邊界。 外部人員有途徑檢查它，這對我來說比另一個 AI 勝利圈更重要。現在是陷阱。

### 正確的證明會回答錯誤的問題嗎？

3:36 Lean 可以接受一個幾乎不要求任何東西的語句的正確證明。 不可能的假設會使定理變得空洞。 更改標題定理下方的定義會削弱 目標。該論文設計了針對此的檢查。 守門員保留一份不讓證明代理寫入的批准規範。 他們可以透過單獨的修訂流程提出更正。 安全性弱化會被升級為潛在錯誤。 證明者的成功聲明在此處無權威。

4:00 人類裁決對受信任假設的變更， 直接或透過其政策，並在每次活動後審查修訂。 專家判斷仍在其中。 代理可以請求不同的任務。 它無法給自己打及格分。

### 什麼捕捉了移動的目標？

4:13 這是承諾的檢查。 Lean 的比較器將定理及其所依賴的每個定義與 受保護的批准副本進行比較。 它還檢查允許的公理並在一個新的核心中重放證明。 因此，悄悄地削弱一個輔助定義會改變被 比較的內容。一個被接受的證明必須確立經批准的目標。 這仍然讓人們負責選擇一個強大的目標和誠實的 假設。對於您自己的 AI 工作流程，請將驗收標準放在

4:37 工作人員編輯權限之外，並單獨審查提議的更改。 Google 的結果使這種分離具體化。 證明撰寫者完成工作； 檢查邊界決定它是否有效。 如果您想閱讀而不是聽我說，The Daily Diff 每天早上都會免費傳送到您的收件匣，網址是 thedailydiff.dev，連結在下方。 每天早上，免費在 thedailydiff.dev 上提供，連結在下方。 所以今天的判決是 SHIP IT。

### 我會發布這個證明工作流程嗎？

4:54 我會發布這個已驗證的證明工作流程，因為經批准的聲明與生成答案的代理保持分離。 我會發布這個已驗證的證明工作流程，因為經批准的聲明與生成答案的代理保持分離。 我會將範圍和假設附加到每個結果。 訂閱、點擊鈴鐺，並在評論中告訴我您是否會蓋上不同的印章。 就是今天的 The Daily Diff。 我是 Axrisi 的 Niko。 負責地合併。

## 來源

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