Claude 為 123 個開源庫生成彙編級形式化證明
Claude 在 123 個真實開源庫的 RISC-V 彙編層面生成了形式化安全證明，作者稱這是首次用 AI 把形式化驗證大規模應用到生產軟體。證明覆蓋所有小於 64 MB 的輸入：在單執行緒靜態二進位制、固定記憶體預算的 RISC-V 執行環境下，程式總能正常退出，不觸發記憶體安全錯誤或斷言失敗。寫證明的過程中 Claude 還發現了數萬億次測試都沒檢出的 bug；
形式化驗證過去只用於航電等關鍵系統，這次首次以 AI 在 123 個開源庫的彙編層面規模化完成，還挖出多年未發現的 bug，對關注程式碼安全與底層系統的開發者有參考價值。
原標題：LLMs are making formal software verification feasible at a much larger scale
閱讀原文
| 評分 | 82 / 85（平均 83，門檻 76） |
|---|---|
| 狀態 | 精選 |
相關報導
Claude 掃描 25 個開源專案，發現 493 個攻擊面問題
Anthropic 公布用 Claude 自動縮減程式碼攻擊面的初步研究：掃描 25 個開源專案、逾 500 萬行 C、C++、Java、PHP、Python 程式碼，發現 493 個問題。Claude 梳理出 1.7 萬個配置項，其中 3842 個與安全控制相關，按預設配置、配置組合、早期可達性三類排查。11 個需認證專案均存在意外可達程式碼：93 處認證前的暴露面、37 處認證前執行或記錄狀態的位置、61 組靜默削弱認證前控制的配置組合。
Anthropic 用 Lean 自動形式化費馬大定理，11 天生成 1300 萬行
數學形式化正從人工轉錄轉為 AI 自動形式化：Anthropic 於 2026 年 9 月 4 日宣布完成費馬大定理的自動形式化，11 天生成 1300 萬行 Lean 程式碼；OpenAI 9 月 8 日公布 Navier-Stokes 強制爆破定理時也附帶了 Lean 形式化。此前 Math Inc. 在 24 維球填充問題上生成約 50 萬行程式碼，Meta 的 ATLAS 專案則自動形式化了 26 本教科書的大部分內容。
七位數學家撰文反對倉促用 AI 形式化全部數學
Jeremy Avigad、Kevin Buzzard 等七位數學家聯合發文，反對在 OpenAI 上週發布後興起的「儘快形式化全部數學」呼籲，認為做得不好會造成持久損害、浪費鉅額資源。文中舉例：Anthropic 稱 Claude 用 1300 萬行程式碼、11 天完成費馬大定理的形式化驗證，Buzzard 稱讚成果卻表示不會停下自己手頭的形式化工作；Math, Inc. 試圖劫持 Viazovska 球堆積形式化專案，原團隊最終棄用 AI 程式碼重做。
Anthropic 擴充套件網路安全驗證計劃，分三檔開放最強模型
Anthropic 將 Project Glasswing 與網路安全驗證計劃合併擴充套件為三檔：Defense、Red Team、Specialized；通過稽核的安全團隊可使用 Claude Opus 5.5、Sonnet 5.5、Mythos 5.1 等最強模型，並減少攔截。Red Team 檔僅限機構、稽核需數週；Specialized 面向電網、航空、電信等關鍵系統，需與美國政府聯合逐家審查。
論文：Lean 驗證 AI 形式化證明不等於原證明正確
arXiv 新論文指出，用 Lean 機械驗證 AI 自動形式化的數學證明，並不能保證原始自然語言證明本身正確。作者 Bastounis、Circelli 與 Hansen 證明，要做到語義忠實的翻譯必須消解自然語言數學文字的歧義，而該問題在可解複雜度指數（SCI）層級中為無窮，比停機問題（SCI=1）更難。