北京時間 2026 年 10 月 23 日約 06:01，Anthropic 官方帳號在 X 指向一篇日期為 2026 年 10 月 22 日的 Frontier Red Team 研究文。Anthropic 稱，與 Theorem 合作，用 Claude 在 RISC-V 組譯層對來自 Google OSS-Fuzz 的真實開源庫形式化證明了安全屬性。DigIntoAI 沒有實測這些證明或流水線。
按 Anthropic 說法，Claude 先修補發現的缺陷，再證明：在 123 個 OSS-Fuzz 庫的 239 個 fuzz 入口點上，對任意小於 64MB 的輸入、以及所建模的 Linux 作業系統回應與記憶體配置，程式不會因記憶體安全錯誤或斷言失敗而崩潰。Anthropic 稱據其所知，這是首次大規模用 AI 對生產軟體做組譯級形式化驗證。Anthropic 稱將公開部分 Rocq 證明與可信元件；Theorem 另稱可為其他開源專案跑同一流水線，並發布可重用的 Claude skill 協助開發者起步。
Anthropic 同時寫明邊界：證明假定單執行緒靜態二進位、固定記憶體預算、RISC-V CPU 與 Linux。需信任的工件包括 RISC-V 與 Linux 行程形式模型、所證定理陳述，以及 Rocq 證明檢查器。Anthropic 寫明這並不等於庫中無 bug；剩餘問題可能落在上述可信元件內，或超出證明範圍。簡言之，LLM 放大的形式化驗證可在這些假設下證明既定的不崩潰規約，但不能單獨保證一切部署場景零缺陷。站內相關說明見 Anthropic 用 Claude 縮小程式碼攻擊面、Anthropic 將 Agent Skills 捐贈給 AAIF 和 METR 與 Redwood 對 OpenAI 內部 agent 監控做了紅隊評估。
我們沒有重現 Rocq 證明，沒有重跑這些 OSS-Fuzz 入口點，也沒有核實 Theorem 的 Claude skill。
