Lean 證明了這個程式是正確的；然後我發現了一個漏洞

背景

這篇文章探討了形式化驗證（Formal Verification）在現代軟體安全中的極限。作者針對一個聲稱經過 Lean 語言完全驗證、保證無誤的 zlib 實作「lean-zip」進行壓力測試，利用 Claude AI 驅動多種模糊測試工具，最終在 1.05 億次執行中發現了兩類重大漏洞：一個是 Lean 執行環境（Runtime）的堆疊緩衝區溢位，另一個則是解析器中導致阻斷服務（DoS）的記憶體耗盡問題。

社群觀點

針對這項發現，Hacker News 社群展開了關於「驗證邊界」與「規格定義」的深度辯論。許多評論者指出，這並非形式化驗證本身的失敗，而是凸顯了規格說明（Specification）與人類意圖之間的落差。有觀點認為，即使程式碼完全符合規格且證明無誤，如果規格本身存在缺陷或過於簡化，最終產出的軟體依然會與預期行為脫節。這種「規格缺口」是驗證過程中最困難的部分，因為隨著系統複雜度提升，精確表達人類意圖的難度並不亞於編寫程式本身，這可能導致開發者產生一種虛假的安全感。

另一派意見則從實務價值的角度切入，認為形式化驗證的真正意義在於「縮小搜尋範圍」。當一個複雜的演算法被證明正確後，開發者在遇到臭蟲時可以果斷排除核心邏輯的問題，轉而專注於邊界條件、假設前提或底層環境的檢查。這種排除法在除錯過程中極具價值，尤其是在 AI 輔助編寫證明的門檻降低後，這種開發模式正變得更加可行。然而，對於文章標題是否過於標題黨，社群內存在分歧。批評者認為作者發現的漏洞並非源於「被證明的程式碼」出錯，而是位於證明範圍之外的解析模組，或是底層 C++ 執行環境的漏洞，這不應歸咎於 Lean 的核心邏輯驗證。

對此，原作者在討論中親自回應，強調從終端使用者的角度來看，整個二進位檔案的安全性才是核心。如果一個標榜「形式化驗證」的系統因為執行環境溢位或解析器崩潰而導致資產損失，對使用者而言，區分漏洞是來自核心邏輯還是執行環境並無實質意義。這場爭論揭示了學術上的「正確性證明」與工程上的「系統魯棒性」之間仍存在顯著鴻溝。社群普遍達成共識：自動化證明工具確實能解決演算法層級的恐懼，但軟體整體的安全性仍高度依賴於對信任運算基座（TCB）的維護，以及對那些尚未被證明的邊緣模組（如解析器）的嚴格審查。

延伸閱讀

在討論中，參與者提到了除了 Lean 之外的其他驗證工具與方法論，包括 TLA+ 與 Z3，這些工具在不同層級的程式驗證與規格檢查中扮演重要角色。此外，討論也提及了 Lean 官方文件中有關細化與 C 語言轉譯（Elaboration and C code generation）的技術細節，這對於理解為何執行環境會出現溢位漏洞至關重要。