rocq

ChainCatcher 消息，人工智能公司 Anthropic 旗下 Frontier Red Team 於 10 月 22 日發布研究，稱大語言模型已能在更大規模上自動撰寫形式化證明。團隊與 Theorem 合作，使用 Claude 在 RISC-V 匯編層對超過 100 個真實開源庫證明安全性質，並稱這是已知首次用 AI 在匯編層對生產軟體做大規模形式化驗證。寫證明過程中還發現了多年未被發現的漏洞。實驗將 Google OSS-Fuzz 中已有的可編譯 fuzz 測試轉為規格：在單線程靜態二進制、固定記憶體預算、RISC-V CPU 與 Linux 等假設下，對小於 64 MB 的任意輸入，程式應正常退出且不觸發記憶體安全錯誤或斷言失敗。數周內，Claude 在修補所發現問題後，對 123 個 OSS-Fuzz 庫中的 239 個入口點證明了上述性質。證明針對編譯後的 RISC-V 指令，約 1.8 億行 Rocq，並由 Rocq 內核檢查。頁面稱，這並不等於這些庫沒有漏洞，剩餘問題可能位於受信任組件或證明範圍之外。頁面還稱，團隊讓 Claude 形式化 RFC 1950，並在 x86 二進制層證明 Linux 內核中的 zlib 實現符合該規格；用 Rust 編寫覆蓋 Python 大子集的解釋器，對超過 170 萬個隨機生成程式與 CPython 行為一致的比例為 99.95%。在 36 個小型驗證任務上，Opus 5.5 證明其中一半所需 token 比 Opus 5 少約 40%。團隊同時指出，證明針對單線程、靜態鏈接的 RISC-V 二進制，且證明檢查器不能判斷規格是否符合現實。