AI 代理在大型軟體系統中發現漏洞的能力越來越強。
Anthropic 顯然對 Mythos 發現漏洞的能力感到非常震驚，因此決定不公開它，認為它「太危險了」（笑）。無論你是否相信這些最新模型的炒作，似乎不可否認的是：
發現安全漏洞的成本正在崩潰，而當今大多數軟體從未設計來承受這種嚴格的審查。我們正面臨一場即將來臨的軟體危機。
面對這場即將來臨的海嘯，最近對形式驗證的興趣日益增加。若我們使用機械化工具陳述並證明程式碼的性質，是否能打造出堅固、安全且穩定的軟體，抵禦這波攻擊浪潮？
Lean 生態系統中的一項最新發展朝這個問題邁進。10 個 AI 代理自主建構並證明了 zlib 的實作 lean-zip，這是一項令人印象深刻的里程碑成果。引用 Lean 首席架構師 Leo De Moura 的話（見此處）：
抱歉帶來 AI 的混亂（Leo 似乎很喜歡這樣），關鍵結果是 lean-zip 不僅僅是另一個 zlib 實作。它是一個經過端對端驗證正確的實作，由 Lean 保證完全沒有實作漏洞。
「驗證正確」到底是什麼樣子？這是其中一個主要定理（github）：
對於任何小於 1 GB 的位元組陣列，呼叫 ZlibDecode.decompressSingle 解壓縮由 ZlibEncode.compress 壓縮的輸出，會還原成原始資料。解壓縮函數正好是壓縮的反函數。這對函數完全正確。
我在一個週末用 AFL++、AddressSanitizer、Valgrind 和 UBSan 指派 Claude 代理測試 lean-zip。經過超過 1.05 億次模糊測試，發現了：
實驗設置相當簡單。我取了 lean-zip 程式碼庫，製作了一個精簡版本，並指派 Claude 代理測試。
具體來說，實驗設置包括：（1）移除所有定理與規範，（2）刪除所有 Markdown 文件，（3）剝除 lean-zip 提供作為原生實作替代的 zlib C FFI 綁定。剩下的純粹是經過驗證的程式碼：Lean 原生定義的 DEFLATE、gzip、ZIP 檔案處理和 tar。任何在此發現的漏洞都代表驗證程式碼中的錯誤。
移除定理和文件的目的是避免讓 Claude 代理知道程式碼已被驗證，避免它因為「程式碼無漏洞」而提前放棄，讓它在盲測狀態下更客觀地分析軟體。
透過 CLI 存取 lean 實作後，我啟動了一個伺服器進行模糊測試，讓 Claude 自由發揮。
一夜之間，Claude 在庫的 6 個攻擊面（ZIP 解壓、gzip 解壓、原生 DEFLATE 解壓、tar 解壓、tar.gz 和壓縮）上啟動了 16 個平行模糊器。它建立了帶 AddressSanitizer 和 UndefinedBehaviorSanitizer 的獨立二進位檔，執行 Valgrind memcheck，使用 cppcheck 和 flawfinder 進行靜態分析，並製作了 48 個針對已知 zlib CVE 模式的手寫攻擊檔案。
總計進行了 105,823,818 次模糊測試，使用了 359 個種子檔案，16 個模糊器運行約 19 小時，發現了 4 個崩潰輸入和 1 個記憶體漏洞。
最重要的發現是一個堆疊緩衝區溢位！但不是在 lean-zip 的程式碼中，而是在 Lean 執行環境本身。
漏洞函數是 lean_alloc_sarray，負責分配所有標量陣列（ByteArray、FloatArray 等）在 Lean 4 中的記憶體：
對於容量為 n 的 ByteArray，分配大小是 24 + n。當 n 接近 SIZE_MAX（64 位元系統為 2^{64} - 1）時，加法會溢位回繞成一個很小的數字。執行環境分配了約 23 字節的緩衝區，但呼叫端會讀取 n 字節進入該緩衝區。
此溢位可透過 lean_io_prim_handle_read 觸發，該 C 函數是 IO.FS.Handle.read 的底層實作：
一個 156 字節的精心製作 ZIP 檔案，其 ZIP64 compressedSize 欄位為 0xFFFFFFFFFFFFFFFF 即可觸發。lean_io_get_random_bytes 中也存在相同模式。此漏洞影響所有 Lean 4 版本，包含最新 nightly（v4.31.0-nightly-2026-04-11）。最簡單的重現程式碼只有 5 行。
編輯：目前已有一個 PR 正在修復此問題。
AFL 也在 lean-zip 自身程式碼中發現了一個拒絕服務漏洞。Archive.lean 中的 readExact 函數直接將 ZIP 中央目錄的 compressedSize 欄位傳給 h.read，卻未驗證其是否超過實際檔案大小（見此處）：
一個 156 字節的 ZIP 檔案聲稱 compressedSize 達數艾字節，導致程序因內存不足（INTERNAL PANIC: out of memory）崩潰，因為 h.read 嘗試分配超出可用記憶體的空間。這確實是一個漏洞：系統的 unzip 會優雅地處理，先驗證標頭大小再分配記憶體，而 lean-zip 則沒有，導致 OOM 崩潰。
這個 OOM 拒絕服務漏洞很直接：檔案解析器從未被驗證。lean-zip 的證明涵蓋了壓縮與解壓流程（DEFLATE、Huffman、CRC32、往返正確性），但 Archive.lean 模組負責讀取 ZIP 標頭與解壓檔案，原始未剝除程式碼中也完全沒有定理。compressedSize 欄位來自不可信標頭，直接用於分配記憶體，未經驗證。這情況讓人聯想到 Yang 等人在 PLDI 2011 發表的 CSmith 研究，該研究發現 CompCert 的驗證優化通過無漏洞，但未驗證的前端卻有漏洞。驗證只在應用範圍內有效。檔案解析器是 lean-zip 未被驗證的部分。
堆疊緩衝區溢位更為根本。lean_alloc_sarray 是 Lean 執行環境中的 C++ 函數，屬於可信計算基礎。每個 Lean 證明都假設執行環境是正確的。此漏洞不僅影響 lean-zip，也影響所有分配 ByteArray 的 Lean 4 程式。
這裡的正面結果才是令人驚訝的。在超過 1.05 億次執行中，應用程式碼（不含執行環境）沒有發現任何堆疊緩衝區溢位、使用後釋放、堆疊溢位、未定義行為（UBSan 清潔）或越界陣列讀取。引用 Claude 對程式碼庫的評價（不知其已被驗證）：
這真的是我分析過最安全的記憶體程式碼庫之一。Lean 的型別系統結合依賴型與良基遞迴，消除了困擾 C/C++ zip 實作的整類漏洞。困擾 zlib 數十年的 CVE 類漏洞在此程式碼庫中結構上不可能出現。
發現的兩個漏洞都位於證明範圍之外。拒絕服務是因缺少規範，堆疊溢位則是可信計算基礎中更深層的問題，即整個證明體系假設正確的 C++ 執行環境（目前已有 PR 處理）。
整體而言，形式驗證帶來了極為穩健嚴謹的程式碼庫。AFL 與 Claude 難以找到錯誤，但仍發現問題。驗證的強度取決於你提出的問題與你選擇信任的基礎。