Anthropic 與 Theorem 在 10 月 22 日公開研究，讓 Claude 把開源軟體原有的模糊測試，轉成可由機器檢查的數學證明。團隊報告已在 123 套程式庫的 239 個測試入口完成證明，並公開其中一部分。這次進展的關鍵，是 AI 交出的安全結論有了能重新檢查的推導過程。
模糊測試會不斷把變形、隨機生成的資料送進程式，尋找造成錯誤的輸入。形式驗證則先寫清楚要保證的性質，再證明所有符合前提的輸入都滿足它。Claude 負責寫證明；最終是否成立，由 Rocq 證明檢查器判定。
對維護解析器、壓縮工具等基礎套件的開發者，這帶來一條值得追蹤的新路：原本只能持續增加測試資料，現在可以嘗試把已有測試提升成對整個輸入範圍的保證。團隊仍須決定測試究竟檢查什麼，這項工作會直接影響證明的價值。
既有測試，成為證明的起點
公開流程文件描述了具體分工。每個任務固定程式庫版本、測試入口與編譯後的執行檔，並準備要證明的命題。模型填入推導，檢查器依指定命題驗收，也會拒絕超出允許清單的假設。
這個分工很重要：模型寫出看似合理的說明，還不足以完成任務。它必須產出 Rocq 能逐步檢查的證明。外界取得公開檔案後，也能使用同一套檢查環境重驗，讓程式安全審查多了一種可交付的證據。
證明能涵蓋多少功能，取決於測試寫得多具體。Theorem 的命題文件舉出壓縮再解壓縮的例子：測試比較還原資料與原始輸入，只要不同就中止。如果相應命題完成證明，保障的就包含這項還原性質。若測試只是呼叫解析器、等它返回，便沒有順便檢查所有解析結果。
嘗試證明的過程也能暴露錯誤。Anthropic 報告指出，模型曾在解壓縮程式發現計數器下溢造成的越界寫入。研究流程允許 Claude 修補程式，再依修補後的版本重新產生命題與證明，串起找錯、修補與驗證。
補丁也必須受到審查。研究團隊有記錄與稽核修改，避免模型藉由移除功能，換取容易成立的證明。維護者仍須判斷程式是否保留原本功能，這也是AI 程式修改審查的重點。
公開成果怎麼用在套件維護
截至本次查核，成果倉庫列出 25 套程式庫、60 個已有證明的入口，包含 JSON 解析、壓縮與網路協定相關測試。這是研究的公開子集，並非公告中的全部成果都已可供下載。開發者可以從自己維護或使用的套件，找到對應命題與建置紀錄。
目前公開證明主要比較原版程式與加入錯誤偵測工具的版本：在指定記憶體預算等前提下，兩者不會走到命題定義的錯誤，且有相同的可觀察行為。這批公開成果尚未包含保證程式一定結束的證明。 它沒有宣告程式會卡住，但也不能拿來承諾服務一定能在期限內回覆。
證明同時綁定特定的靜態 RISC-V Linux 二進位檔。更換處理器、編譯方式或程式版本，就需要重新對應；執行環境的形式模型也有自己的假設。因此，直接採用同名套件的網站，不能把這份證明當成整個服務的安全認證。
我認為這項研究最實際的意義，是讓測試逐漸成為可累積、可重驗的安全資產。對台灣維護開源套件或共用內部元件的團隊，值得先把關鍵行為寫成明確測試，留下版本與建置資訊。這能改善現有測試，也替未來的證明建立目標。
Theorem 已開放符合條件的開源專案免費申請 OSS Verify，優先處理被廣泛使用的基礎軟體。核心維護者可提交專案與建置資料，由團隊審查資格；過程若發現問題，會先私下提供給維護者。
一般網站開發者則可把它當成依賴套件的新證據來源，搭配既有原始碼安全審查。它與安全掃描服務回報修正狀態回答的問題不同：這裡提供的是指定程式、指定命題的可檢查證明。
常見問題
全部研究成果都能下載嗎？
目前只公開子集。本次查核時，倉庫列出 25 套程式庫、60 個已有證明的入口，並未釋出全部成果。
採用這些套件就能免測試嗎？
不能。證明涵蓋指定建置與測試入口的命題，應用程式自己的整合行為仍需測試。目前公開證明也沒有保證每次執行都會結束。
開源專案如何申請驗證？
由核心維護者向 OSS Verify 提交專案資料、建置環境與測試建置腳本。符合資格的專案免費，Theorem 會審查使用情況、維護狀態及安全重要性。
參考來源
- Anthropic：LLMs are making formal software verification feasible at a much larger scale（2026-10-22）
- Theorem：Where the proofs come from（未標發布日，2026-10-25 查核）
- Theorem：What gets proven（未標發布日，2026-10-25 查核）
- Theorem：OSS Verify: proofs about OSS-Fuzz fuzz targets（未標發布日，2026-10-25 查核）
- Theorem：Free formal verification for open source.（未標發布日，2026-10-25 查核）