Specification and Model-checking of the ZKsync Governance Protocol | Igor Konnov
三句話摘要
使用 Quint 規範語言與三層模型檢查技術，對 ZKSync 治理協議（ZKGovernment）進行形式化規範與漏洞驗證。 --- 形式化規範的價值不在於「取代代碼審計」，而在於強迫你把協議邏輯說清楚，然後讓機器用三種不同深度的工具幫你找人眼容易忽略的角落案例。 1. 協議理解先於技術驗證
重點整理
重點- 1
1. 協議理解先於技術驗證
- 2
光看 Solidity 程式碼很難寫出正確的不變量；先用規範語言明確協議邏輯，才能讓後續的模型檢查有意義的目標。
- 3
2. Quint 的函數式建模讓「平行未來比較」成為可能
- 4
因為所有狀態轉換都是無副作用的純函數，可以在同一個不變量中同時計算多個未來狀態（如軟凍結 vs 硬凍結），不需要引入時序邏輯（Temporal Logic）即可驗證複雜的協議行為。
- 5
3. 三層工具形成成本遞增的覆蓋策略
- 6
隨機模擬成本低但覆蓋率有限；隨機符號執行藉助 Z3 SMT Solver 提升反例覆蓋；有界模型檢查在特定深度內窮舉所有執行路徑。三者互補，先跑便宜的再跑昂貴的。
- 7
4. 規範與代碼審計是互補關係
- 8
模型檢查無法取代代碼層級的形式驗證，但可以更快速地重現外部提交的潛在問題，並在修復後確認問題已消除，大幅縮短驗證週期。
- 9
--
實用技巧與重點
乾貨- 協議實體：代幣大會（Token Assembly）、守護者（Guardians）、緊急升級委員會（Emergency Upgrade Committee）、安全理事會（Security Council）
- 規範語言：Quint（基於 Leslie Lamport 的時序邏輯操作，採現代語法）
- 執行環境：TypeScript 撰寫，需 Node.js + VS Code；模型檢查需 Java
- 隨機符號執行後端：Z3 SMT Solver（透過 Apalache 模型檢查器）
- 規範規模：約 40 個動作、45 個不變量
- 隨機模擬：100,000 次執行 × 最多 30 步交易 = 3 小時
- 隨機模擬：1,000,000 次執行 ≈ 30 小時
- 隨機符號執行：1,000 次符號執行 × 最多 30 步交易 = 更長時間，但發現更多錯誤
- 有界模型檢查（6 步）：半天，發現 4 個不變量撰寫問題
- 有界模型檢查（9 步）：10 天，無新增問題
- 凍結類型：軟凍結（Soft Freeze）、硬凍結（Hard Freeze），均由安全理事會觸發
- 模型檢查器發現的反例類型：安全理事會啟動升級 → 72 小時後守護者批准 → 800+ 小時後執行
- --
結論
結論“形式化規範的價值不在於「取代代碼審計」，而在於強迫你把協議邏輯說清楚，然後讓機器用三種不同深度的工具幫你找人眼容易忽略的角落案例。”
完整解析
詳細ZKSync 的治理協議（ZKGovernment）設計了四個相互制衡的實體：代幣大會負責提出合約升級提案，另外三個實體（守護者、緊急升級委員會、安全理事會）則負責審核與執行。安全理事會額外擁有凍結第二層的權力。這個協議的邏輯複雜度遠超單純的智能合約溢位問題，光靠讀程式碼很難掌握所有可能的執行路徑，因此講者決定引入形式化規範工具。
講者採用 Quint 語言將協議重新描述為狀態機。Quint 不了解 EVM 或 Solidity，這迫使開發者必須顯式建模所有需要的元素——包括區塊時間戳、合約狀態、L2 抽象狀態與歷史變量。每個智能合約被表示為一個記錄（record），合約行為被定義為純函數（無副作用、無異常），接受 EVM 狀態與合約狀態作為輸入，返回新狀態或錯誤訊息。當多個函數組合為「動作」（action）時，才引入非確定性——例如非確定性地選擇交易發送者。整個協議最終被定義為大約 40 個動作的狀態機。
Quint 最具特色的建模技巧在於不變量的撰寫。由於所有操作都無副作用，可以在單一不變量中計算多個分支未來：例如在同一個狀態下，分別嘗試執行軟凍結與硬凍結，再比較兩個未來的合法性，完全不需要引入時序邏輯（Temporal Logic）。這讓原本用英文寫成的需求文件，能被相對直接地翻譯為可機器驗證的規範。
驗證策略採用三層遞增成本的方法。隨機模擬器最便宜，100,000 次執行只需 3 小時，但覆蓋率有限。隨機符號執行將數據選擇的任務交給 Z3 SMT Solver，能找到更多邊界反例。有界模型檢查器最昂貴，在 6 步交易深度內窮舉所有路徑只需半天，卻揪出 4 個不變量撰寫錯誤；擴展到 9 步則耗費 10 天，但未發現額外問題。值得注意的是，有界模型檢查器發現的問題，在大量隨機模擬與符號執行後仍未被察覺——印證了不同工具各有盲區、必須並用的原則。
---
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
