Claude 形式驗證研究帶來可由 Rocq 檢查的程式證明，但保障取決於規格、執行檔與環境模型。本文釐清已證明的範圍、公開證明與加入專案的 skill，說明開發者為何仍需檢查輸入限制、未覆蓋的性質與部署條件。
Anthropic 在 10 月 22 日公布與 Theorem 合作的研究，讓 Claude 替開源程式撰寫形式證明，再由 Rocq 檢查器核對。想拿它保證自己的服務沒 bug，先看證明涵蓋的執行檔、輸入與條件。官方研究
證明涵蓋哪些程式？
作者報告涵蓋 123 個開源程式庫的部分測試入口：針對小於 64 MB 的輸入，證明既定規格中的崩潰不會出現。前提包括 RISC-V／Linux 模型、單執行緒、靜態連結與固定記憶體預算。
形式驗證把「程式應滿足什麼」寫成可證的規格。它能論證範圍內所有輸入，但規格與環境模型也得正確；漏寫的性質不會自行獲得保障。研究未驗證每個入口，記憶體檢查工具 ASan 也抓不到所有記憶體錯誤，不能把這讀成整個程式庫已無 bug。研究限制
公開成果能拿來做什麼？
Theorem 已公開部分 Rocq 證明與核對方法。倉庫明示，證明針對該版本的二進位檔，以及測試入口能觸及的程式碼；即使證明成立，錯誤結果或記憶體洩漏仍可能存在。這批公開證明也沒有保證程式一定終止，不能據此排除無限執行。
公開的 Linux 程序語義與前提列出模型缺口，例如只描述單一執行緒，並假設其他程序不會改動所建模的檔案。若服務在不同架構、動態連結或多執行緒環境運作，就得重新確認證明是否適用。
想讓自己的開源專案加入流程，可先讀 add-project skill。它協助維護者定義入口、輸入與性質，準備建置檔並提出加入專案的 PR；Theorem 再處理所建二進位檔的證明，安裝 skill 本身不會讓任意程式獲得保證。
若目前還沒寫清楚預期行為，可從小樣本驗收練習開始：測試檢查選定案例，形式證明論證明確前提下的性質。該篇教你整理案例與預期答案，沒有教授形式驗證。