Anthropic 以 Claude 對 123 個開源函式庫的 RISC-V 組合語言做形式化驗證，並發現多年未被察覺的錯誤

Anthropic 於官網發表研究，與合作夥伴 Theorem 利用 Claude 在組合語言層級（RISC-V）對 123 個開源函式庫進行形式化驗證，據其所述為目前已知首次以 AI 將形式化驗證大規模應用於production軟體的組組合語言層級。研究團隊證明這些程式在特定假設下，對所有小於 64 MB 的輸入，且在每一個建模的 Linux 作業系統回應與記憶體配置中，都會正常結束，不會觸發記憶體安全錯誤或斷言失敗。這些假設包括：程式以單執行緒靜態二進位檔執行、使用固定記憶體預算、運行於 RISC-V CPU 並搭配 Linux OS。 驗證的做法是將各函式庫既有、可編譯的測試套件自動轉換為規格，以「此測試套件必定通過」作為正確性定義。在撰寫證明的過程中，Claude 另外發現了數年來儘管經過數兆次測試仍未被察覺的錯誤。 Anthropic 表示會公開部分證明及 RISC-V 與作業系統語意，供外界驗證與重用；Theorem 也願意為其他開源專案執行相同流程，並發布供開發者入門使用的 Claude skill。研究團隊指出，這距離修復所有可能的錯誤仍很遠，但比以往更接近目標。