Claude 形式驗證百餘開源程式庫：239 個入口的證明，保證了哪些安全性？
Claude 形式驗證研究替123個開源程式庫的239個測試入口撰寫Rocq證明。本文解釋測試轉規格、RISC-V執行條件、證明檢查器與共享證明成本，分清特定安全保證與整個軟體無漏洞的距離。
一個程式通過幾兆次測試，仍可能在某個罕見輸入崩潰。測試能找出反例，卻很難把所有可能輸入都跑過一次。
Claude 形式驗證研究在 2026 年 10 月 22 日公開，嘗試把這個問題改寫成數學命題，再讓獨立於模型的證明檢查器逐步核對。
Anthropic 與 Theorem 報告，數週內替 123 個開源程式庫的 239 個測試入口完成證明，核心是指定條件下的輸入不會讓程式崩潰。
條件包括小於 64MB 的輸入、單執行緒與特定 RISC-V/Linux 執行環境。它擴大了可證明的規模，卻沒有宣稱整個程式庫在所有平台都無漏洞。
對已有測試入口、希望確認關鍵依賴特定性質的團隊，公開產物值得驗證。只有看到模型說「已安全」的結果，仍不足取得這種保證。
這次進展的起點，是把現有測試想找的錯誤，變成一個可由機器查證的精確命題。
Claude 形式驗證如何把測試轉成可證明的規格？
團隊沿用開發者寫好的模糊測試入口，將「這個測試不崩潰」編成針對執行檔的命題。模糊測試也叫 fuzzing，會不斷產生或修改輸入，嘗試撞出錯誤。
入口像替程式開的一扇測試門。開發者指定資料如何送進去，也會把自己在意的失敗變成崩潰，讓測試引擎能辨認哪個輸入有問題。
這種方法很有效，卻主要靠不斷找反例。沒有找到崩潰，代表目前試過的路徑沒有揭露它，不能直接推出每個還沒試到的輸入都安全。
Anthropic 的完整研究改用現有測試定義規格。規格就是精確寫出程式應滿足什麼條件，讓「正確」不只是一句模糊要求。
團隊將程式庫和測試編譯成 RISC-V 執行檔，再配上處理器與 Linux 程序的形式模型，產生待證命題。RISC-V 是一種處理器指令架構，描述晶片可以執行哪些基本動作。
因此，主要證明對準的是編譯後的指令，不是只讓模型閱讀原始程式，再寫一段「看起來沒問題」的報告。這讓檢查對象更接近真正執行的產物。
這套形式驗證做法也不必先替每個大型應用寫出完整功能規格。它從開發者已表達在測試裡的要求開始，例如不越界、壓縮後解開要還原原資料。
若測試規定資料往返必須相同，違反就會崩潰，那麼證明測試永不崩潰，也就涵蓋了那個往返要求。保證有多強，取決於測試和命題實際要求什麼。
這提供一條逐步擴張的路徑：先處理清楚且重要的性質，再增加其他規格，而不必宣稱一次解決「整套軟體什麼都正確」。
規格定好之後，模型負責寫出推導，接受與否則交給另一套系統。
Claude 寫證明，Rocq 檢查器究竟核對什麼？
Rocq 核對證明能否推出精確命題，不是根據 Claude 的文字解釋判斷可信度。它是一套形式證明工具，會依自己的邏輯規則檢查每一步。
形式驗證的這個分工很重要，因為模型可能產生很有說服力、實際卻不成立的推導。把接受條件交給檢查器，能減少只憑語氣或另一個模型同意就判定成功的情況。
但檢查器回答的問題有邊界。它可以核對「在這些假設下，證明是否滿足這個命題」，不會自動知道人類真正想要的功能是否被命題完整表達。
例如，若只證明某個測試入口不崩潰，就不能從中推出網頁服務必定正確驗證使用者身分。兩者需要不同規格，不能因同屬安全問題就互相代替。
這次報告的證明約有一億八千萬行 Rocq 程式，典型單份約六十萬行，對應的執行檔指令長度中位數約一萬八千條。證明文字和被驗證的產品程式碼，是兩種不同產物。
證明比原程式大很多，並不代表模型替開源專案新增了同樣數量的功能。大量內容是為了把編譯指令的行為和安全命題接起來，供檢查器核對。
因此，這也改變形式驗證的人工審閱重點。人類不必逐行相信模型寫出的每個理由，卻需要核對命題是否是自己要的、機器模型是否合理，以及檢查器是否值得信任。
由檢查器接受，也不等於已有外部研究者把整批結果獨立重跑。前者是證明系統的驗證方式，後者是另一項可追查的實際執行，不能在新聞裡合併成同一個承諾。
當這些角色分清楚，龐大證明就有可理解的用途。不過，證明數量仍要連同入口和輸入條件閱讀。
123 個程式庫、239 個入口與 64MB，各代表哪一層範圍？
這些數字量的是形式驗證已完成的目標，範圍由測試入口與部署條件界定。入口數可以超過程式庫數，因為一個程式庫可能有多個測試入口。
研究使用 Google OSS-Fuzz 生態系裡的開發者測試。這些入口原本就設計來找出維護者在意的崩潰，但不代表它們涵蓋了程式庫所有功能與呼叫順序。
小於 64MB 則是命題的輸入範圍。即使把上限固定，可能的位元組組合仍多到無法靠逐一測試實際窮盡，形式證明的價值是用推導涵蓋這個集合。
若要增加上限，必須改動命題並重新取得證明。不能只因上限看起來像一個設定值，就在報導裡自行延伸成任意大小都成立。
主要形式驗證結果還假設程式是單執行緒、靜態連結、記憶體預算固定，並在指定的 RISC-V/Linux 模型下執行。這些是保證能成立的前提，而非可以省略的安裝細節。
其中記憶體檢查仰賴 AddressSanitizer，也就是在程式執行時偵測部分記憶體錯誤的工具。它會把某些越界等行為變成錯誤，但不會發現所有記憶體問題。
因此，證明沒有觸發這套檢查，不能擴寫成排除所有種類的漏洞。測試的範圍、檢查工具的能力和形式模型，會一起決定最後保證的範圍。
截至 10 月 23 日，公開證明儲存庫列出二十五個程式庫、六十個入口的證明。這是釋出的子集，和整體研究報告的規模不同。
官方說明，有些產物可能揭露尚未修補的錯誤，所以沒有把所有證明直接公開。讀者可以核對已發布內容，不應把整體數字解讀成同樣數量都已供外部重跑。
在這些明確範圍內嘗試完成證明，還可能暴露原本測試很難撞到的錯誤。
延伸閱讀：PHP 緊急修補兩項遠端執行漏洞：OpenAI 與 Wiz 如何找到問題，網站該確認什麼？
為何寫證明也會找到錯誤，修補又如何避免鑽漏洞？
當形式驗證的命題證不下去，模型可能找到罕見反例並提出修補。這讓驗證不只是最後蓋章，也成為尋找錯誤的一種過程。
官方舉例，有一個解壓縮錯誤，需要約二十MB且排列非常特殊的輸入才會出現。常見模糊測試通常對較小輸入變異，未必容易走到這個條件。
另一類問題需要特定的呼叫順序，或非常深的巢狀輸入。這些案例說明，長期沒撞出來不等於不存在，也解釋了為什麼嘗試建立全範圍推導會找到不同線索。
但不是所有證明失敗都代表原程式一定有漏洞。模型可能還沒找到推導方法，或形式模型不夠完整，所以需要分辨反例、工具限制和證明搜尋失敗。
為了讓工作不中斷，團隊允許 Claude 修補發現的錯誤，再針對修改後的執行檔重新產生命題與證明。這表示最後的保證有時對應修補版本，不能全部算成原始碼從來就安全。
這項權限也可能被鑽漏洞：如果直接刪掉功能、讓程式立刻結束，不崩潰的命題可能變容易，卻失去使用者原本需要的行為。
研究因此對修補設置代價，鼓勵證明哪些輸入行為被改變、改動範圍有多小，並記錄及稽核修補。這是團隊採用的控制方式，不是模型不可能走捷徑的證明。
對工程團隊，可借鏡的是把功能要求和安全命題一起保留。即使修補後通過檢查，也要知道新命題是否仍描述要交付的工作，不能只讓成功標記取代行為核對。
這樣的形式驗證和修補需要大量生成工作，因而讓重用既有成果變得很有價值。
共享證明如何省成本，40% 與 17% 又測了什麼？
官方在三十六個較小任務觀察到，新模型與共享工作區可減少 Token，但這是特定內部實驗的結果。Token 是模型處理與生成文字的計量單位。
這組測試取自真實模糊測試程式，每題給三次獨立單代理嘗試，各有五百萬 Token 預算，第一個完成的嘗試決定何時算證明成功。
在這個設定下，Opus 5.5 證出一半任務所需的 Token，約比 Opus 5 少四成。這個結論對應指定完成比例與任務集，不能改寫成每份證明都固定便宜四成。
另一個實驗讓代理互相取用已寫好的證明，平均少用 17% Token。有些原本單獨失敗的目標，也在能利用共享成果後完成。
原因不只在對話協作。許多程式包含相同的啟動與檢查機制，證明這些共通部分後，下一個目標可以沿用，不必從頭重新解釋所有指令。
這和軟體重用函式庫相似：重複工作的成本降低，新的工作就能集中在不同之處。但重用仍需要確認前提相符，不能把一份證明不加檢查貼到任何程式上。
Theorem 的路線說明希望把這種重用擴到更多軟體依賴。那是逐步建構已驗證生態系的計畫，不是宣布所有常用套件已經完成。
對判讀成本，最有用的是保留任務、模型與共享方式。只有一個節省比例，無法替每個團隊估出完成自己目標的總費用。
當成本下降、覆蓋擴大，最後仍需把形式模型和實際機器之間的連接核對清楚。
從 RISC-V 到實際服務，信任邊界還在哪裡？
形式驗證的命題、處理器與作業系統模型、證明檢查器都需要正確，才能把已證性質對應到真實執行。這是工作能否落地的關鍵，不只是證明檔案能否編譯。
主要結果使用靜態連結的 musl 環境，許多實際服務卻在 x86 或 ARM 上動態連結 glibc。它們的指令和執行條件不同，不能直接照搬主要研究的保證。
開放的 Linux 程序模型也明示自己尚不完整，含有未由模型檢查的假設。把這些前提公開，讓其他人知道哪裡可以挑戰，比只交出一個「驗證成功」更可追查。
檢查器本身也要在實際的軟體與硬體上運行。因此，形式驗證不是消除所有信任，而是把原本要相信的整段程式推導，收斂到較明確的命題、語意模型與檢查系統。
公開版本還明示，這次釋出的證明沒有證明程式必定終止。因此，不出現指定錯誤和一定完成執行，是兩個不同性質，不能把前者直接當成不會無限執行或所有功能都正確。
例如服務需要在時限內回應，這個要求就必須另行表達。形式驗證能涵蓋哪些行為，來自命題的內容，而非證明檔案很長，或生成它的模型很強。
所以採用形式驗證時，先把「不會發生哪種錯誤」和「一定完成哪項工作」分成不同要求，再核對目前的產物涵蓋哪一項。這能避免把安全性與可用性混成一個成功標記。
呼叫端也是另一條邊界。程式庫自己的測試入口安全，不代表其他應用一定正確使用它。若外部程式傳錯資料或違反函式條件，仍可能在呼叫端造成問題。
我會建議已有關鍵依賴與明確安全要求的團隊，先挑一個目標，核對執行版本、命題與已公開證明。若部署環境不同，就先列出差在哪裡，再評估如何補上。
這種採用方式不需要等待「所有軟體都可證明」才開始，也不需要把一次成功擴大成全面安全。先取得一項條件清楚、能被重查的保證，就已經改變了確認軟體行為的方法。
延伸閱讀：OpenAI 公開 722 份 AI 數學稿件：372 組成果與 Lean 驗證怎麼看？
Claude 形式驗證常見問題
模型說自己檢查過，算形式驗證嗎？
不算。這次由模型產生形式證明，再交 Rocq 檢查器核對指定命題，不能用自然語言自評代替。
有證明就能停掉所有測試嗎？
已證命題只涵蓋特定範圍。部署差異、其他功能與呼叫端行為，仍需要相符的驗證方式。
123 個程式庫的全部證明都公開了嗎？
沒有。官方釋出子集，並保留可能揭露未修補漏洞的內容，應以公開清單核對。
可以直接套到其他 CPU 嗎？
主要成果的條件是 RISC-V/Linux。換架構需要對應的形式模型和證明，不能只改執行檔名稱。
先驗一個精確性質，再擴大可證明的軟體範圍
這次成果顯示，AI 可以協助把原本昂貴的形式證明擴到更多既有軟體，並在嘗試證明的過程中找出罕見錯誤。
對團隊有用的下一步，是確認一個公開產物、命題和部署前提是否相符。保證說得越精確，才越容易知道它解決了什麼，下一個缺口又在哪裡。
想追蹤 AI 資安研究、可驗證產物與開源工具更新，可免費訂閱 AI 郵報，並從官方公開清單核對最新版本。
