Fuzzing vs Formal Verification — Panel discussion | Web3 Security Summit
三句話摘要
智能合約安全中 Fuzzing 與形式驗證（Formal Verification）的適用邊界與實戰取捨。 Fuzzing 是入門快、成本低的必要基礎，形式驗證是覆蓋深層邏輯錯誤的進階武器，兩者不互斥，但正確定義 invariant 才是決定兩種方法是否有效的真正關鍵。 1. 預算有限時 Fuzzing 優先，但 invariant 定義才是核心
重點整理
重點- 1
1. 預算有限時 Fuzzing 優先，但 invariant 定義才是核心
- 2
不論使用哪種工具，若 invariant 定義錯誤或無意義，兩種方法都不會產生價值。Fuzzing 在相同時間內可得到更廣的覆蓋率，且開發者只需 2-3 天訓練即可獨立應用。
- 3
2. 形式驗證對多條件交叉路徑有結構性優勢
- 4
當合約涉及複數個前置條件才能觸發的漏洞時，Fuzzer 需花費大量算力才能到達，而形式驗證透過抽象化（procedure summary）可以系統性地探索這些路徑。
- 5
3. Fork 測試是 Fuzzing 的殺手鐧，形式驗證難以複製
- 6
Fuzzing 可直接 fork 主網狀態對真實 Chainlink、Uniswap 等合約進行測試，極為精確；形式驗證處理外部呼叫時需手動注入 bytecode 或提供函式摘要，稍有偏差則會驗證出錯誤結論。
- 7
4. 差分模糊測試（Differential Fuzzing）是數學邏輯錯誤的首選武器
- 8
針對複雜數學公式（固定小數點運算、精度損失），可在 Python 用成熟庫實作相同邏輯，再讓 fuzzer 大量隨機比對兩者結果，能揪出即使不在審計範圍內的函式庫漏洞。
實用技巧與重點
乾貨- 工具名稱
- Fuzzing 框架：Foundry、Wake（Ackee，Python 生態）、Echidna、Medusa
- 形式驗證工具：Certora Prover（CVL 語言）、Kontrol（Runtime Verification，Solidity 語法）、Halmos、EthBMC
- Mutation Testing：Gambit（Trail of Bits 開源）
- 視覺化除錯：Runtime Verification Solidity Symbolic Debugger（視覺化展示所有分支狀態）
- 具體數字
- 1,000 行 Solidity 合約：手動審計約 1 週，加上引導式 fuzzing campaign 約額外 +30%（≈2 人天）
- 形式驗證啟動學習曲線：Fuzzing 2-3 天可上手；形式驗證需更長，且需數學歸納法直覺
- 以太坊質押合約 bug：驗證時發現 32 ETH（當時約 10 萬美元）會因 Vyper 編譯器缺少輸入驗證而導致質押者無法正確註冊
- 方法名稱
- 引導式 Fuzzing（Guided Fuzzing）：測試者指定函式呼叫序列，縮小狀態空間，比黑盒 fuzzing 效率更高
- 差分模糊測試（Differential Fuzzing）：雙實作比對找精度錯誤
- Procedure Summary（函式摘要抽象化）：形式驗證中處理不可驗外部呼叫的方法
- Mutation Testing：對合約插入隨機 bug，測試不變量能否偵測
- 真實案例
- Ethereum 質押合約（Vyper 版）：Runtime Verification 以形式驗證找到 Vyper 編譯器未驗證輸入的 bug，最終促使以太坊基金會改用 Solidity 重寫
- Iore Protocol：Ackee 用差分模糊測試對比 Solidity 函式庫與 Python 同功能庫，發現審計範圍外的精度損失 bug
- Compound + Uniswap 交互：形式驗證團隊在 Compound 部署前發現其與 Uniswap 交互時的未預期行為（使用 procedure summary 建模 Uniswap 行為）
- 可操作流程
- 先寫單元測試 → 整合測試 → 達到 90-100% 覆蓋率
- 加入引導式 fuzzing（定義 invariant 與流程序列）
- 將同一份 property test 餵入形式驗證工具（如 Kontrol），不需重寫規格
- 在 CI Pipeline 執行形式驗證（夜間建置），不阻斷本地開發週期
- 使用 Gambit mutation testing 驗證 invariant 本身是否有效
結論
結論“Fuzzing 是入門快、成本低的必要基礎，形式驗證是覆蓋深層邏輯錯誤的進階武器，兩者不互斥，但正確定義 invariant 才是決定兩種方法是否有效的真正關鍵。”
完整解析
詳細這場圓桌討論匯集了 Trail of Bits、Runtime Verification、Ackee Security 與學術界四方代表，圍繞一個在智能合約安全領域長期存在的實戰問題：當資源有限時，開發者與審計師應該優先選擇模糊測試（Fuzzing）還是形式驗證（Formal Verification）？
討論一開始就直指核心矛盾：形式驗證在理論上能提供最高的正確性保證，但學習曲線陡峭，且對工具熟悉度要求高。Trail of Bits 的 Josselin Feist 明確表示，若客戶只有有限預算（例如兩週），Fuzzing 能在同等時間內取得遠高於形式驗證的覆蓋率。原因在於 Fuzzing 框架（如 Foundry、Wake）允許開發者直接用 Solidity 撰寫 invariant，沒有語言隔閡；而形式驗證工具（如 Certora 的 CVL 語言）雖然功能強大，卻需要額外的學習成本，甚至需要數學歸納法的直覺才能有效運用。Runtime Verification 的 Shafranek 則補充：他們的 Kontrol 工具選擇讓開發者直接用 Solidity 撰寫 property test，並同時將同一份規格餵給 Fuzzer 與形式驗證引擎，試圖消弭這道門檻。
在技術適用邊界上，各方的分歧與共識同樣清晰。Fuzzing 的顯著優勢在於 fork 主網能力：可直接拉取鏈上合約的真實 bytecode 進行測試，這讓涉及 Chainlink、Uniswap 等外部整合的測試極為精確。Ackee 的 Joseph 特別強調「引導式 Fuzzing」（Guided Fuzzing）與黑盒測試的差異：測試者主動指定函式呼叫序列，大幅縮小狀態空間，讓算力集中在真正有意義的路徑上。差分模糊測試（Differential Fuzzing）則是另一個殺手鐧——用 Python 成熟庫實作相同的數學公式，讓 fuzzer 對比兩者結果，能有效發現固定小數點精度損失，甚至揪出不在審計範圍內的第三方函式庫 bug（如 Iore Protocol 案例）。形式驗證的優勢則在多條件交叉觸發的深層邏輯錯誤：學術代表 Moody 指出，當漏洞需要多個前置條件同時滿足才能觸發，Fuzzer 在有限時間內極難抵達該路徑，形式驗證卻能透過抽象化（procedure summary）系統性地涵蓋——Ethereum 質押合約案例就是最佳佐證，Runtime Verification 在部署前發現了 Vyper 編譯器未驗證輸入的 bug，該問題在傳統代碼審計中幾乎不可能被發現。
最後，所有人都在一個問題上達成共識：不論選擇哪種工具，「寫出正確且有意義的 invariant」才是真正的難關，佔整體工作量的 80-90%。一個驗證「合約名稱不變」的 invariant 毫無安全價值；而一個定義錯誤的 invariant 更可能給人虛假的安全感。正因如此，多位講者建議在撰寫任何形式化規格之前，先收集開發團隊、審計師、競賽研究員等多方視角的自然語言描述，再逐步轉化為可執行的測試。Gambit（mutation testing 工具）與 Solidity Symbolic Debugger（視覺化狀態空間）則是驗證 invariant 品質、發現未覆蓋分支的輔助利器。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
