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

Published: 2026-11-11

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

Canonical: https://thedailydiff.dev/zh-HK/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 你可以在不相信模型勝利宣言的情況下檢查結果。 單獨的檢查會捕捉悄悄更改問題的情況。 我們將追溯到定義。 今天是 11 月 10 日星期二，這裡是 The Daily Diff。 AlphaProof Code 是 Google 的框架，用於在 人類指導下編寫軟件規範，並使用 AI 代理生成已驗證的證明。 這項研究針對 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 的結果使這種分離具體化。 證明撰寫者完成工作； 檢查邊界決定它是否有效。 如果你寧願閱讀這份報告而不是聽我說，那麼每日差異會 每天早上免費發送到你的收件箱，網址是 thedailydiff.dev，連結在下方。 所以今天的判決是 SHIP IT。

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

4:54 我會發布這個已驗證的證明工作流程，因為已批准的聲明與 產生答案的代理保持分離。 我會將範圍和假設附加到每個結果中。 訂閱、點擊鈴鐺，並在評論中告訴我你是否會蓋上 不同的印章。這就是今天的差異。 我是 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