2026 年 10 月 22 日，Anthropic 的 Frontier Red Team 在官網發布了〈LLMs are making formal software verification feasible at a much larger scale〉，介紹與 Theorem 合作的 Claude 形式驗證研究。團隊報告：在數週內，為 123 個開源函式庫的 239 個測試入口完成特定安全性質的證明。這個消息值得看，但「證明通過」四個字，要連同它承諾的範圍一起讀。
先看原文做了什麼，再對照公開證明庫，最後回答一個實用問題：你該如何判斷這份保證能否用在自己的軟體上？最值得帶走的改變，是 AI 的成果開始附帶可由另一套確定規則檢查的證據；最需要避免的誤讀，是把入口的證明擴張成整個產品的安全認證。
Claude 形式驗證：把「試過很多次」推進到「這個命題成立」
想像一個收取圖片的函式。測試像把各種正常、破損與刻意變形的圖片送進去，觀察是否出錯；形式驗證則先寫出精確規則，再證明在規則涵蓋的情況下，錯誤不會發生。兩者回答的問題不同，也各自依賴你選了哪些檢查。
Google 的 OSS-Fuzz 文件說明，它把模糊測試引擎、Sanitizer 與分散式執行接起來。這次研究沿用開發者已有的 fuzz harness，也就是把外部輸入送進函式庫的一小段測試程式。如此一來，研究者不必先替一整套軟體重新寫完所有功能的數學規格。
工作流程是：把測試程式及依賴編譯成 RISC-V 執行檔，使用形式化的機器與作業系統模型描述其行為，再讓 Claude 構造證明。Rocq 官方介紹確認，Rocq 能以相對小的認證核心檢查形式證明。這裡的價值在於：生成證明的模型可以嘗試許多路徑，最後是否接受，交由證明檢查器依既定命題判斷。
因此，模型回答得有自信，不是這套方法的驗收條件。不過，核心檢查的是形式命題；「命題是否對準真實需求」仍是另一份工作。若要補上「先寫成功條件」的背景，可接著讀 AI Evals 入門。
239 個入口與公開 60 個入口，要分開對帳
原文的 239／123 是研究團隊報告的整體結果。截至 2026 年 10 月 24 日，本文讀到的 Theorem 公開證明庫固定版本列出的是 25 個函式庫、60 個入口的證明，使用 Rocq 9.2.0。公開子集與整體研究數量不同，不能把前者說成已讓所有成果都接受了公開重跑。這是模型供應商與驗證服務團隊共同公布的成果；兩方的共同報告，也不能算成兩次獨立重現。
公開庫的說明把保證拆得更細：在記憶體預算等前提內，帶 Sanitizer 的版本與普通版本具有相同的可觀察行為，並排除命題所定義的錯誤。若測試程式內有以 assert 檢查的性質，那項檢查也會進入要證明的內容。這讓證明可能超過單純「沒有偵測到越界」，但具體超過多少，要看那個入口實際寫了什麼。
這也解釋為何研究選擇編譯後的程式：證明對準實際二進位產物，減少把原始碼另譯成模型時的一層落差。代價是保證緊綁那份產物與環境。你換了編譯選項、依賴或架構，就應重新確認證明究竟還指向什麼。
本文查閱公開文件與研究附件，未在本機重跑完整 Rocq checker。公開庫提供檢查路徑，代表證據可供他人查驗；它本身不等於本文已完成獨立重現。讀者應把研究者報告、公開工件與第三方重跑結果當作不同層次的證據。
有個關鍵修正：「不崩潰」不能直接讀成「一定會結束」
An agreement statement does not exclude a run that never ends.
中文：行為一致性命題不排除永遠不結束的執行。
Theorem，OSS Verify 公開證明庫 README，固定版本 98e995d4dace。
這句出自公開庫 What a proof does not say。同一節明確說明，該版本沒有證明 halts 命題，因此不排除不終止的執行。研究主文在介紹段落使用「正常結束」的概括語氣；實際採用公開成果時，應以各份定理的精確陳述為準，不能把兩種性質併在一起。
對工程決策而言，差別很具體：上傳一個檔案後，服務可能沒有越界、沒有觸發指定錯誤，卻一直占著工作。排除記憶體錯誤和保障可用性，並不自動是同一張證書。要對抗資源耗盡，還得把終止、時間或資源上界納入你真正需要的保證。
同樣地，「測試入口能到達的程式」也不等於「整個函式庫」。未被這份命題涵蓋的 API、呼叫順序與使用方式，不能靠函式庫名稱相同就接收保證。這不是否定證明，而是避免把一張有地址的收據拿去報銷另一筆交易。
Claude 形式驗證的安全邊界：先看輸入、機器與模型
“Formally verified” does not mean “bug-free.”
中文：「經過形式驗證」不代表「沒有任何錯誤」。
Anthropic，原文 Limitations。
原文與 技術附件把主要實驗限制在小於 64 MiB 的輸入、單執行緒、靜態連結的 RISC-V／Linux 程式，並帶有記憶體預算等前提。主文使用 MB 的簡寫，附件的正式描述採 MiB；閱讀精確上限時，應沿著附件與各定理往下查。這些條件必須與 239／123 一起出現。原文限制段落也明說，ASan 並不偵測所有記憶體安全錯誤；因此通過這些檢查，不能改寫成排除所有類型的記憶體問題。
此外，該證明庫指定版本的 LPS 範圍文件公開列出模型落差，例如執行緒、訊號處理與檔案系統的涵蓋限制，以及模型不自行檢查的假設。數學推導正確，並不會自動讓模型缺少的現實行為補進來。
我會把信任分成三個問題：定理寫對了嗎？機器與系統模型貼近部署環境嗎？檢查器及其工件讀取鏈可信嗎？公開庫的信任清單還包含二進位轉換工具及檢查包裝層，不能只留下「相信 Rocq」四個字。這些元件的集中審查，才是大批生成證明能帶來的工程優勢。
另一個邊界是需求本身。例如，假設影像處理程式把顏色算錯但沒有觸發任何斷言，僅證明不崩潰，無法替色彩正確性作保。若要保證「解碼後內容符合格式」，就要把對應功能性規格寫進命題。這是本文的示例，用來說明保證取決於規格。
證明途中找到漏洞，與修補後保持功能，是兩個驗收點
研究團隊表示，嘗試證明的過程也找到了漏洞，並允許 Claude 修補後重新產生待證規格。這讓形式驗證兼具找錯與建構保證的用途；即使某個目標最終未完成證明，過程中的反例仍可能有修補價值。
但模型可以改程式，也會帶來目標投機：假設把所有輸入直接拒絕，某種不崩潰條件可能更容易滿足，產品功能卻被掏空。原文註腳交代，團隊以懲罰修補、鼓勵說清行為改動範圍及稽核補丁來降低這個風險。這是研究者描述的控制方式，不能改寫成已證明每份修補都符合使用者意圖。
對採用者，我建議把三份東西綁在一起保存：證明對應的執行檔、實際定理、修補前後的功能差異。若少了第三項，「新的程式符合新的規格」可能仍沒回答「原來該做的事是否保住」。這也與 Alter 權限驗收所強調的問題相通：合法完成一個動作，仍要確認做的是正確對象與正確範圍。
成本下降有線索，還不是所有專案的報價單
上圖呈現原文用來支持效率改善的實驗。附件的任務設計說明，這 36 題由真實程式縮小而來，替換了 libc、限制輸入至 64 bytes，並使用簡化的 mini-ASan。主文報告 Opus 5.5 完成半數任務所需 token 比 Opus 5 少約 40%；這是該組設計下的比較，不能直接當成任意函式庫都能省下四成總費用。
另一條改善路徑是重用。上圖把不同程式的證明組成放在一起，讓人看見共通啟動流程與執行期的重複工作。主文另報告共享工作區的任務少用 17% token。它支持「既有證明可能攤薄下一份成本」這個方向，但沒有提供所有專案維護期的通用節省比例。
附件的專家判讀也沒有把證明很長當作純粹勝利：代理反覆展開暫存器、記憶體位置等細節，可能需要更好的模組化抽象才能走向更複雜程式。已被檢查的定理不因冗長而失效；真正未定的是這種寫法往外擴張後，生成、檢查與維護的成本如何成長。
原文還介紹其他路線，包括壓縮格式的功能性驗證，以及用 Verus 證明 Rust 撰寫的 Python 子集直譯器。附件對後者的表述是「當它回傳結果時，結果符合形式語義」，再用測試連結到 CPython 行為。這個例子再次提醒我們：形式規格內的正確性、是否終止，以及與真實系統的對應，應逐項讀取。
AlphaLab 的判讀：該增加的是證據，不是「安全」標籤
一、我同意的突破：生成端可以昂貴，接受端應有清楚規則
AI 很適合大量嘗試，但軟體供應鏈需要能留下來的驗收依據。把成果交給形式檢查器，讓後來的人能針對同一份命題與工件再檢查，會比只交一段「我已修好」的說明更有價值。要衡量這項進步，應追蹤可查驗工件、有效覆蓋範圍與重驗成本，而非證明檔案的行數。
二、我存疑的外推：一個研究流程，何時能變成日常維護？
研究的結論預期形式驗證會像今天的 fuzzing 一樣普及。這是前景判斷，還需要後續資料。我的對帳方式是：上游小改一次，多少既有證明仍可用？失效後需多少成本修復？換成實際部署架構後，能保住多少性質？如果這幾項改善，普及的論點才會更有說服力。
三、證明的地址，必須跟著出貨的位元組走
你在 LiteLLM 供應鏈攻擊解析看到的是「看過的原始碼」與「收到的成品」之間的落差。這份研究則讓人看見另一種綁定需求：證明即使成立，部署出去的也必須是它指向的那份產物。版本名稱相同仍不夠，還要核對雜湊、建置及依賴紀錄。
四、把專家時間移向規格與信任邊界，才可能擴大收益
當機器能產生大批證明，最稀缺的判斷可能轉到「值得證明什麼」。挑一個容易通過卻無關緊要的命題，成果可以漂亮但收益有限；挑一個真正卡住部署的性質，再明確寫出前提，才讓生成能力變成安全價值。這是我從公開工件得到的判斷，而非研究已量化的收益。
下一步：拿到「已驗證」成果，先問五件事
- 是哪份產物？記下入口、程式雜湊、依賴與建置方式。
- 證明哪個命題？分清不觸發錯誤、行為一致、功能正確與終止。
- 前提是什麼？列出輸入大小、記憶體、架構、執行緒與系統模型。
- 修補改了什麼？確認使用者需要的正常行為仍被保留。
- 下一版怎麼重驗？把檢查接進版本更新，記錄失效與修復成本。
評估 Claude 形式驗證時，若你正在設計 AI 開發流程，可以先從 Agent Harness 的狀態與停止條件整理驗收位置，再選一個小而關鍵的解析或轉換功能。先把「在什麼條件下，什麼必須成立」寫成一句可被反駁的話。能說清這句話，再看一份證明是否真的替你回答了它。
接著閱讀
左右滑動查看更多推薦
