Vitalik 撰文倡議形式驗證：AI 寫程式搭配數學證明，安全性可高於人工

Vitalik 5/18 在自家部落格發了一篇〈A shallow dive into formal verification〉，講法很直接：AI 會讓駭客找漏洞更快，但只要把 AI 寫的程式碼配上「形式驗證」（用機器可驗證的數學證明確認程式行為正確），整體安全性反而會比人工寫的程式更高。zksecurity 的 Yoichi Hirai 把這條路徑叫做「軟體開發的最終形態」。

Vitalik 特別點名 Ethereum 基礎建設、ZK 系統、共識機制、後量子密碼學是最該用形式驗證的場景，因為一個漏洞就能搬走幾億美元（直接點名 2 月的 Bybit 15 億美元駭客之痛）。不過他也提醒形式驗證不是萬靈丹：可能只證了一部分而漏掉關鍵 bug、可能規格本身寫錯、可能 Lean 自己有 bug、甚至硬體的旁通道攻擊都能繞過正確的程式。這條路要走通，需要 Lean、AI、零知識證明三邊一起進化。