軟體開發的最終形態降臨？以太坊共同創辦人 Vitalik Buterin 今（18）日發表長文，深入探討「形式驗證（Formal Verification）」與 AI 結合的巨大潛力。他指出，使用低階語言撰寫程式，並透過 Lean 語言進行電腦自動驗證，將能賦予以太坊 EVM 與 ZK 系統前所未有的安全性與效率。Vitalik 斷言，儘管 AI 短期內可能加劇漏洞攻擊，但在形式驗證的輔助下，防禦方最終將取得壓倒性優勢。
（前情提要：Vitalik：別試著對抗 AI，而是為人類建一個庇護所）
（背景補充：Vitalik對話肖風香港：以太坊系統簡化最優先，太複雜到僅剩 50 人懂，開發者與用戶會嚇跑）
在區塊鏈的世界裡，程式碼的漏洞往往意味著數以千萬計的資金在一夕之間蒸發。為了解決這個致命痛點，以太坊共同創辦人 Vitalik Buterin 給出了他的終極解方。
Vitalik 於今（18）日發布了一篇名為《淺談形式驗證（A shallow dive into formal verification）》的最新文章。他觀察到，過去幾個月來以太坊前沿研究圈正快速崛起一種全新的程式設計典範：直接使用極低階語言（如 EVM bytecode 或組合語言）撰寫程式，並搭配 Lean 語言來編寫電腦可自動檢查的「數學證明」。
Vitalik 引用開發者 Yoichi Hirai 的說法，將這種結合譽為「軟體開發的最終形式」。
什麼是形式驗證？將程式碼變成「數學定理」
簡單來說，形式驗證就是以電腦可以自動嚴格檢查的方式，來撰寫數學定理的證明。
Vitalik 舉例說明，不同於人類憑直覺推導，在 Lean 語言中，開發者可以將加密通訊協定（如 Signal）的安全性轉換為定理。透過證明 X3DH 密鑰交換的安全性與 AES 實作的正確性，電腦能「端到端（end-to-end）」地保證：除了持有私鑰的用戶外，沒有任何人能讀取訊息。這種將程式行為化為嚴謹數學驗證的方式，大幅提升了系統的 Trustlessness（無需信任）。
對抗 AI 駭客！扭轉資安防禦劣勢的終極武器
在加密貨幣與 ZK（零知識證明）領域，Bug 是極其危險的。智能合約出錯會導致資金被盜且無法追回，而 ZK 系統的 Bug 甚至可能在無人察覺的情況下被惡意利用。隨著未來進階 AI（如 Claude Mythos）的出現，AI 將具備自動發掘「零日漏洞（Zero-day）」的可怕能力。
面對這種安全威脅，許多人感到悲觀，認為防禦永遠勝不過攻擊。但 Vitalik 提出了強烈的反對與樂觀的願景：
「AI 尋找漏洞只是過渡期的挑戰。在形式驗證的幫助下，我們終將進入一個由『防禦方』取得大幅優勢的新均衡。」
Vitalik 堅信，形式驗證讓我們有能力「證明所有東西都是正確的」。
在以太坊中的實際應用：極致效率與安全
文章深入探討了形式驗證目前在以太坊生態中的落地應用，特別是在 EVM 實作與 ZK-EVM 領域。目前開發社群正嘗試用 Lean 語言撰寫 RISC-V 組合語言版本的 EVM，並證明其在 Gas 計算與堆疊操作上的絕對正確性。
Vitalik 描繪了一個令人興奮的未來工作流程：由 AI 負責生成極高效的低階組合語言程式碼，接著再由形式驗證來確保這些程式碼 100% 正確。這意味著開發者可以重回高效的低階開發，同時依然保持系統的可理解性與絕對安全性。
雖然形式驗證目前仍面臨證明複雜度高、耗時長，以及規格（Specification）本身可能寫錯等限制，但 Vitalik 預言，AI 將大幅加速證明的撰寫過程，讓形式驗證從小眾技術走向主流。這不僅將催生更安全的網際網路與去中心化系統，更能完美實踐 Cypherpunk 的終極理想。
📍相關報導📍
Vitalik反思以太坊本質：最大價值是「公共佈告欄」，智能合約只為方便標準化
