AlphaProof Code 驗證 Signal 核心：六百萬行 Lean 如何改變 AI 程式驗收？
AlphaProof Code 以Signal核心協定展示可機器檢查的形式證明。解析六百萬行Lean、人類安全規格、歷史漏洞回放與信任邊界，理解程式驗收能保證什麼。
AlphaProof Code 把 AI 寫程式的驗收問題往前推了一步。Google DeepMind 在 11 月 10 日介紹框架，並以 Signal 核心協定實作說明如何產生可由機器核對的證明。
這裡的證明不是模型再回答一次程式沒有問題，而是把安全主張寫成明確條件，再交給 Lean 的證明核心檢查推導是否成立。
官方案例累積超過六百萬行 Lean 證明，花費四週完成工作，但時間與規模都是這個案例的描述，不能直接套到每個軟體專案。
更重要的是，證明能保證的範圍取決於人類先寫下的規格、程式模型與假設，沒有涵蓋的攻擊仍然不會自動消失。
這項研究較實際的意義，是讓關鍵程式的安全主張留下可重驗的依據。它支持團隊把驗收說得更清楚，沒有替整個通訊產品提供無限範圍的安全承諾。
要看懂這種差別，先分清楚測試找到錯誤與形式證明確認性質各自做了什麼。以下依 2026 年 11 月 12 日查核的官方公告與研究產物說明。
AlphaProof Code 和一般測試差在哪裡
測試觀察選定輸入，形式證明則在寫明的模型與條件下確認性質成立。兩者都能增加信心，回答的問題與需要付出的準備不同。
一般測試可以把幾組訊息送進程式，看輸出與預期是否相同。測試經過的情況有具體結果，沒經過的情況卻不會因為前幾組成功，就自動獲得相同保證。
形式驗證則先描述程式行為與要成立的條件，再用數學推導建立關係。這讓研究者能對一類情況提出主張，前提是模型與安全規格有把真正關心的內容寫進去。
Google DeepMind 原始公告以 Signal 核心協定實作為案例，展示如何讓 AI 產生大量證明，再由獨立的檢查機制核對。
通訊協定是雙方交換訊息時遵守的規則，核心實作則是把規則變成可執行程式。對這類工作，驗收不只問訊息能否送達，還涉及哪些資訊應該保持不被外部得知。
這也是案例值得關注的原因。若只看功能測試，訊息順利送到就像工作完成，但安全性還需要對攻擊者能力、秘密資料與程式行為建立更明確關係。
形式證明不能免除這些定義工作。它可以嚴格核對寫下來的主張，卻不會自動知道團隊漏掉了哪一種現實風險，證明範圍因此成為閱讀研究時的重點。
要讓確認有意義，第一步應先把安全主張寫對，再研究如何產生證明。這也說明為什麼研究裡仍保留人類對規格的責任。
為什麼人類仍要先決定證明什麼
一個過弱的條件也可能被完整證明，所以規格的安全意義仍須由人判斷。規格就是程式應滿足的明確要求，寫得精確與寫得足夠，是兩個都要處理的問題。
例如，只要求程式最後回傳某種格式，可能完全沒有約束秘密資料如何被使用。即使這項要求被證明成立，也不能由此推出通訊內容得到保護。
官方研究把安全性主張與依賴條件列為需要信任與審核的部分。證明代理處理的是固定規格下的推導，不能為了讓證明通過，隨意把原本要求改弱。
若研究過程發現規格需要修訂，也要經過另外的判斷與記錄。更改可能是在修正定義問題，也可能不小心減少保證，因此不能把修改藏在大量自動產生的內容裡。
這種安排讓工程團隊能分清責任。人類先決定值得保護什麼，檢查規格是否對應目標，AI 再探索如何把這些要求和程式行為連起來。
人類參與不代表每一行證明都必須逐字手寫。較有價值的投入，是集中在安全意義、假設與程式外部環境，讓大量重複推導能交給工具處理。
這也和一般程式審查相通。若需求原本就含糊，後面再多測試或檢查，也可能只是在確認錯誤目標；把要求寫清楚，才能讓自動化工作有可採信的方向。
規格固定後，AI 與證明核心才各自承擔能被查核的工作。六百萬行的規模來自這個分工，信任依據則是固定規格與可核對的推導。
六百萬行 Lean 是怎麼被核對的
AI 可以大量探索推導，接受與否仍由獨立的證明核心按形式規則檢查。Lean 是證明助理，讓定義、主張與推導能以機器可檢查的形式表達。
對讀者來說，可以先把它理解成一套嚴格的推導規則。模型提出的每一步推導，都需要符合這套規則與已建立的前提，語氣是否自信不會改變檢查結果。
官方說本次案例累積超過六百萬行 Lean 證明，完成時間為四週。這展示自動化探索能處理很大的推導工作量，但不代表所有專案都能用相同時間完成。
不同專案需要建立的程式模型、既有定義與信任假設不一樣。案例進度也不能直接換算成人員節省比例，除非有相同任務與完整工作量的對照。
證明核心的角色，是核對形式上的有效性。若模型產生錯誤步驟，檢查無法通過，就需要再修正，這讓產生證明與接受證明形成可分離的流程。
核對通過後仍要回看前提
但形式有效仍依賴前提。把一個重要條件列為假設，相當於把它留在需要信任的部分，不能因為後續推導很多，就說所有前提也已經被證明。
因此，閱讀研究產物時，值得先找主張、假設與依賴關係，再看證明如何串起來。行數可以描述工作規模，無法單獨描述安全覆蓋有多完整。
公開的形式驗證研究產物讓外部研究者有機會檢查這些關係。證明鏈成立後，還要回到案例本身確認它覆蓋哪一部分程式。
Signal 案例涵蓋什麼，歷史漏洞測試又證明什麼
研究瞄準核心協定實作的特定安全主張，歷史漏洞回放用來檢查框架能否辨識已知錯誤。這兩部分回答不同問題，不能混成現行產品發現新漏洞的新聞。
Signal 是完整的通訊產品，包含用戶端、伺服器、作業系統互動與許多功能。驗證核心協定實作，不表示這些層次與所有未來版本都一併被涵蓋。
核心程式的證明仍有重要價值，因為它對到一段明確而關鍵的資料處理。但保證範圍應沿著研究模型理解，不能由產品名稱出現就推成整個產品永遠沒有漏洞。
官方也描述重新引入兩個已修復的歷史錯誤，在隔離版本裡測試系統能否產生可檢查的錯誤證據。這提供了負面案例，避免只證明一個已整理好的安全版本。
已知錯誤被重新放回來，是實驗設計的一部分。它不代表這些錯誤仍存在於使用者手上的現行版本，也不是要求讀者根據這則研究自行推定產品正在受攻擊。
這類測試的意義，是看框架是否能區分滿足與違反安全要求的程式。若安全版與帶錯版都得到相同結論，就需要重新檢查規格或模型是否漏掉關鍵差異。
對工程團隊而言，負面案例也能幫助檢查安全主張是否太弱。把一個應被拒絕的程式放進流程，能觀察驗收是否真的對到原本想保護的性質。
這些結果值得參考，但程式外部的環境與密碼假設仍影響保證範圍。要理解證明為什麼不能無限延伸，就得看哪些條件仍留在信任邊界內。
信任邊界如何限制安全保證
證明需要依賴規格、密碼元件與系統環境的假設，這些條件不會因為證明很長就消失。信任邊界就是把已由推導處理的部分，和仍需另外相信或驗證的部分分開。
例如，程式呼叫某個密碼功能時，模型可能依賴它符合指定行為。要把整個系統的保證擴大，就需要知道這個功能來自哪裡、依賴哪些安全假設，以及如何對接實際程式。
密碼學安全通常也建立在明確的攻擊者能力與數學假設上。本次研究保留這些密碼學前提，在寫明條件下檢查程式與安全主張的關係。
系統環境同樣重要。作業系統、外部函式與執行條件若不符合模型假設，形式推導的適用範圍就可能改變，這些需要在交接文件裡清楚呈現。
某些攻擊面也可能不在特定模型內，例如旁通道與模型之外的秘密記憶體處理。旁通道是從時間、資源等外部現象取得資訊，與只看程式邏輯的威脅描述不同。
形式驗證因此讓安全承諾可以被具體討論。團隊可以指出已驗證什麼、還依賴什麼，並依風險決定下一步補足哪一部分。
同樣地，程式更新後不能只沿用舊版本的結論。修改是否影響模型、規格與證明，需要重新檢查，才能把驗收證據對到使用中的程式版本。
因此，工程團隊導入時要先選出值得明確描述與持續維護的核心性質。證明工作能不能跟著更新，是長期採用的重要條件，而不只是單次產出量。
工程團隊應該先改哪個驗收習慣
先列出資料流與安全不變條件，再評估能否建立可重驗的模型，比先追求證明數量有用。安全不變條件指程式不管走到哪一步，都應持續遵守的要求。
對一段關鍵工作，團隊可以先問秘密從哪裡進來、允許送到哪裡，以及哪些狀況應拒絕處理。這些問題先寫清楚，才知道後面的測試與證明是否抓到重點。
接著再分開目前已有的證據。功能測試提供具體輸入結果，程式審查提供人員判斷，形式驗證則對指定模型提出可檢查主張，各自對應不同範圍。
如果一開始就要求整個產品一次完成全部證明，容易把大量時間花在邊界不清的工作。先挑影響大、規格可明確描述的核心部分，較能判斷準備成本與維護負擔。
本次公告公開的是研究框架與產物，沒有宣布一套對所有團隊正式開放、可直接購買的通用服務。導入規劃應從研究成果與自身能力評估，不預設有現成介面替所有程式完成驗收。
對正在使用 AI 寫程式的團隊，現在就能改善的是保留版本與驗收依據。模型說已修好之後，仍要能指出哪個要求被滿足，以及這份結果對應哪一次改動。
相關背景可以接著閱讀以下兩篇，分別理解形式驗證的覆蓋範圍，以及代理取得系統權限後會出現哪些額外邊界。
延伸閱讀：Claude 形式驗證百餘開源程式庫：239 個入口的證明，保證了哪些安全性？
延伸閱讀：EMBRACE 研究：AI 助理內嵌瀏覽器，為何會讓網頁跨進本機權限？
AlphaProof Code 常見問題
完成形式證明就代表 Signal 完全沒有漏洞嗎？
研究針對明確模型與安全主張下的核心實作，不能覆蓋整個產品、所有作業環境與未來改版。閱讀保證時，應一起看規格、假設與排除範圍。
六百萬行證明比少量證明一定更安全嗎？
行數描述工作規模，安全意義取決於主張是否重要、規格是否足夠，以及推導依賴哪些假設。一個弱條件被完整證明，仍可能沒有保護真正關心的資料。
歷史漏洞測試表示現行版本有新漏洞嗎？
官方把已修復錯誤重新放進隔離版本作為測試，目的是檢查框架辨識錯誤的能力。這和現行產品的新漏洞公告不同，不能混為一談。
讓安全主張能被重新檢查
AlphaProof Code 展示的方向，是讓 AI 大量處理證明探索，再由獨立規則核對，並由人類對安全意義負責。對關鍵程式，先把主張、版本與信任邊界寫清楚，才能決定哪些部分值得進一步形式化。
訂閱 AI 郵報，持續追蹤程式驗證與 AI 工程研究。下一次看到模型宣稱程式安全時，先找出它完成了哪項可重驗要求，再判斷那份證據能支持多大的承諾。
