Trail of Bits 以代理建立 MASM 稽核工具，公開 95 項 Lean 正確性證明

Trail of Bits 於 9 月 18 日公開 Miden 零知識虛擬機的稽核案例：團隊在正式審查前，以六個月讓代理協助建立語言伺服器、反編譯器、靜態分析與 Lean 執行模型。這次公開的是一套把模型產出交給程式分析和證明核心檢查的工作方法。[案例原文](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

Miden 的組合語言 MASM 以堆疊傳遞運算元，閱讀程式時必須追蹤每一步資料位置。公開的語言伺服器把指令造成的堆疊變化、反編譯結果與型別診斷帶進編輯器，也能檢查有限域元素被當成三十二位元整數、卻缺少驗證的情況，讓人類與代理共用同一組分析線索。[工具儲存庫](https://github.com/trailofbits/masm-lsp)

依團隊報告，靜態分析找到四百多處可改善型別驗證的位置，以及一項高嚴重度問題：模數運算未充分驗證證明者提供的餘數，可能讓 Falcon 簽章驗證遭繞過。這些位置不能直接等同四百個可利用漏洞；報告也未提供可據以判定目前部署風險的完整修補版本表。[稽核發現](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

形式化驗證則把 MASM 程序轉成 Lean 定義，在虛擬機的可執行語意模型上證明正確性。公開儲存庫列出九十五個已檢查程序，分布於六十四、一百二十八、二百五十六位元整數及 word 操作，並提供指定 Lean 版本與逐模組建置方式，讓外部研究者有重驗起點。[證明與驗證步驟](https://github.com/trailofbits/masm-lean)

證明範圍仍須逐項閱讀。例如六十四位元右旋程序的定理明列「位移量除以三十二的餘數不為零」這項前提；通過證明核心，只能支持指定模型與前提下的性質，不能推廣成整部虛擬機已獲完整安全保證。團隊也說明，人工仍須審查定理是否描述了真正要驗證的行為。[定理限制](https://github.com/trailofbits/masm-lean)、[人工審查方式](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

對工程團隊而言，可借鑑之處是把代理的探索成果沉澱成能重複執行的工具。導入時應先固定被分析程式與語意模型的版本，再檢查未支援的語法、定理前提及回歸測試；後續最值得追蹤的是程式更新後，這些證明與診斷能否持續成立。