把 Ethereum 寫成
可被機器檢查的證明

測試能告訴你程式在一些情況下會不會壞；正式驗證想追問的是：核心規則能不能被寫成一個機器也無法含糊帶過的論證。

來源：Zero Knowledge Podcast Episode 396 ｜原始發表日期：2026 年 3 月 25 日

SCROLL

PART 1 ｜測試不是證明

程式跑過，不等於規則已被窮盡

Alex Hicks 在訪談中談的正式驗證，起點不是「少一個 bug」的口號。一般測試會選擇輸入、跑出結果，再比對預期。它能抓到很多錯誤，也永遠只能覆蓋被選到的情況。只要輸入空間夠大，仍可能有一個沒被測到的角落，剛好破壞安全性或經濟規則。

正式驗證的作法不同：先把系統應滿足的性質明確寫下來，再用證明助手檢查從定義到結論的每一步。它不會保證「整個世界都安全」，但能讓某個精確命題不再依賴直覺、文件描述或人工覆核。

核心差別：測試問「這些案例有沒有成功？」；證明問「在寫清楚的假設下，這個性質是否必然成立？」

PART 2 ｜ lean Ethereum 想接起整條堆疊

訪談是 lean Ethereum 系列的最後一集。它關心的不只是某個密碼學原語是否正確，而是從 RISC-V、zkVM、電路、編譯器到證明系統的連接處。每一層都可能把上一層「看似正確」的結果，轉換成下一層不再等價的實作。

因此，目標不是替每個元件貼上一個「已驗證」標籤，而是逐步縮小元件間的未說明空隙。例如，一段程式被編譯後，是否仍維持原先的語意？一個電路是否正確表達要驗證的計算？一個證明系統接受後，究竟能推出什麼？

規格先寫清楚系統要保證什麼

實作模型把程式、指令或電路轉成可推理的定義

機器檢查用 Lean 等工具逐步確認推導

組合邊界確認跨層轉換沒有偷換原意

PART 3 ｜工具的取捨，本身也是設計

Hicks 區分了證明助手與自動求解器的工作方式。像 Lean 的系統讓研究者把定義、引理與推導留成可檢查的文本，適合建立長期可被重讀、修改與組合的知識。自動求解器則能在特定形式下快速找出滿足條件或反例，適合把一些子問題交給自動化處理。

兩者不是二選一。難題在於知道什麼要被人明確表達、什麼可交給工具搜尋，以及工具成功後留下的產物能否被另一個檢查器驗證。這關係到未來維護：當編譯器、曲線或協定版本改變，團隊能否知道哪個假設失效，而不是只得到一串過期的「通過」。

可讀性人是否能追到一條安全主張依賴哪些定義。

可重跑性工具更新後，證明是否還能被獨立檢查。

可組合性不同團隊的成果能否接成更大的保證。

PART 4 ｜進度不該只用完成率衡量

訪談沒有把正式驗證說成一次完成整個 Ethereum 或整個 ZK 堆疊的工程。它描述的是長期工作：選定一段重要邊界，定義它，證明它，再把經驗帶到下一段。證明範圍、成本與維護責任都需要明確寫下來，否則「形式化」也可能只是新的宣傳詞。

對使用者和協定設計者，這帶來一個較實際的閱讀方式：不要只問某專案是否用了 Lean 或 ZK。更應問它究竟證明了哪個性質、前提是什麼、實作與規格的距離還有多遠，以及遇到升級或例外時誰負責重新檢查。

正式驗證不是替系統加上一張「不會出錯」的貼紙，
而是把最不能含糊的主張，
寫成機器也必須逐步核對的證明。

來源訪談聚焦 lean Ethereum 的研究方向；它描述的是逐步擴大可檢查範圍的工作，而非已完成的全堆疊安全保證。

Zero Knowledge Podcast Episode 396 保留 Alex Hicks 對 lean Ethereum、證明助手、zkVM 與正式驗證進度的完整討論。