zakrad/certora-prover-skill

Certora Prover (CVL / EVM)

Certora Prover 用於對智能合約進行形式化驗證：您編寫 CVL（Certora 驗證語言）規格來描述屬性（規則與不變量），Prover 會針對所有輸入和狀態證明它們成立，或者返回一個具體的反例 (CEX)。

核心心智模型 — 請先閱讀此部分：

• 證明，而非測試。 與單元測試或模糊測試（僅抽樣少量輸入）不同，Prover 會對模型中允許的每個輸入、呼叫者和儲存狀態進行符號推理。
• 完備但不完整。 在模型範圍內不會遺漏違規情況，但可能超時，且僅檢查規格實際斷言的內容。一個空/弱的規格什麼也證明不了。
• 「驗證通過」= 在模型範圍內且根據您的假設，沒有反例。 每個 require、摘要、循環展開和樂觀標誌都會縮小模型範圍。綠色勾號的強度完全取決於這些假設 — 正確設定假設是全部關鍵。

工作流程：從頭開始驗證應用程式

1. 安裝 + 金鑰。 pip install certora-cli；設定 CERTORAKEY。（→ references/running-and-config.md）
2. 專案佈局。 將合約放在 src/ 下，規格放在 certora/specs/ 下，每個目標一個 .conf 檔案。（→ references/running-and-config.md）
3. 撰寫第一個健全性/參數化規則。 從小型開始：一個參數化規則（method f）斷言在任何函數呼叫後某個基本屬性成立，僅用於確認編譯器（harness）編譯並執行。（→ references/rules-invariants.md，references/spec-patterns-cookbook.md）
4. 執行。 certoraRun MyContract.conf（或直接傳遞 .sol/.spec），然後開啟報告連結。（→ references/running-and-config.md）
5. 閱讀報告。 檢查反例的呼叫追蹤和儲存；修正規格或確認真正的錯誤。（→ references/running-and-config.md，references/debugging-and-timeouts.md）
6. 添加不變量 + 幽靈變數。 陳述真正的屬性：歸納不變量，加上用於會計的幽靈變數/鉤子（例如 sumOfBalances == totalSupply）。（→ references/rules-invariants.md，references/hooks-and-ghosts.md）
7. 加強健全性 + 合理性。 始終執行 --rule_sanity basic；審查每個摘要和假設；移除或合理化任何不健全的捷徑。（→ references/soundness-and-approximations.md，references/methods-and-summaries.md）
8. 突變測試。 使用 Gambit 確認您的規則確實能捕獲注入的錯誤 — 能在突變中存活的規格代表假設過多。（→ references/debugging-and-timeouts.md）

10 秒快速入門

pip install certora-cli
export CERTORAKEY=<您的金鑰>

// Counter.spec — 證明 increment() 嚴格增加數值
methods {
    function get() external returns (uint256) envfree;
}

rule incrementIncreases(env e) {
    uint256 before = get();
    increment(e);
    assert get() > before, "increment 必須增加計數器";
}

certoraRun src/Counter.sol:Counter \
    --verify Counter:certora/specs/Counter.spec \
    --solc solc8.20 \
    --rule_sanity basic \
    --msg "counter increment"

如何使用此技能 / 參考文件地圖

閱讀與目前任務匹配的文件：

• references/cvl-language.md — 需要 CVL 語法時閱讀：檔案結構、類型（mathint/env/method/calldataarg/storage）、型別轉換及其健全性、運算子/量詞、require vs assert vs satisfy vs havoc、函數與定義，以及如何呼叫合約方法（env，envfree，withrevert，lastReverted）。
• references/rules-invariants.md — 撰寫規則時閱讀：規則、參數化規則（method f）、satisfy 見證，或帶有 preserved 區塊和 requireInvariant 的歸納不變量。
• references/methods-and-summaries.md — 配置 methods 區塊時閱讀：條目種類、envfree/optional、完整的摘要目錄 + 健全性表格、表達式/幽靈摘要、以及多合約設定（using、links、DISPATCHER）。
• references/hooks-and-ghosts.md — 需要鏡像儲存或證明會計時閱讀：儲存/操作碼/瞬態鉤子、幽靈變數/函數、總和幽靈變數、以及 persistent 幽靈變數。
• references/running-and-config.md — 安裝、執行 certoraRun、撰寫 .conf 檔案、選擇標誌、佈局專案或解讀網路報告時閱讀。
• references/spec-patterns-cookbook.md — 需要現成配方時閱讀：訪問控制、「什麼可以改變」、餘額總和、單調性、框架條件、狀態機、往返測試、交換性、還原條件、以及單元測試風格的規則。
• references/advanced-defi-patterns.md — 驗證真實協議且基本食譜不足時閱讀：ERC4626 金庫匯率單調性（交叉乘法、無免費午餐、預覽邊界）、AMM k-不變量與無價值提取、借貸償付能力/健康狀況/「無壞帳」與抗鎖定活躍性、獎勵漂移會計、作為 CEI 的重入攻擊、以及大規模基於角色的訪問控制 — 每個慣例都歸因於其來源的生產倉庫（Morpho/OZ/Aave/Certora）。
• references/tooling-and-ecosystem.md — 將 Certora 整合到 CI（GitHub Actions、快取、門控 PR）或決定哪個工具適合某個屬性時閱讀：Certora vs Halmos vs Foundry（不變量/模糊測試）vs Echidna 的決策指南，附有何時使用哪種工具的權衡。
• references/learning-resources.md — 想要深入學習或入門時閱讀：精選外部連結 — RareSkills/Certora 教學、官方文件、講座、以及值得作為實例閱讀的真實世界公開規格倉庫（Morpho、Aave、OpenZeppelin、Compound）。
• references/soundness-and-approximations.md — 決定假設與斷言時閱讀：健全/悲觀與不健全/樂觀、循環/雜湊/破壞近似、樂觀標誌家族、通過規則保證的內容、以及健全性審查檢查清單。
• references/debugging-and-timeouts.md — 規則空洞、緩慢或可疑時閱讀：--rule_sanity、超時緩解（摘要、拆分、範圍約束）、TAC 難度報告、Gambit 突變測試、VSCode LSP、以及「我應該相信這個通過嗎？」檢查清單。
• cheatsheet.md — 想要一頁快速參考時閱讀：最常用的 CVL 關鍵字、規則/不變量骨架、常見的 certoraRun 標誌、以及一目瞭然的主要陷阱。
• examples/ERC20.spec — 想要一個完整的工作規格時閱讀：methods 區塊、餘額總和幽靈變數+鉤子、供應量不變量、參數化/完整性/還原/可加性規則、以及鑄造訪問控制。
• examples/ERC20.conf — 需要一個可執行的 JSON5 配置模板涵蓋所有常見金鑰時閱讀（files、verify、solc、packages、optimistic_loop、rule_sanity、...）。

黃金規則 / 常見陷阱

• require ≠ 還原。 require 假設一個事實（修剪模型）；它不檢查合約是否還原。要推理還原行為，請使用 withrevert + lastReverted。
• 注意空洞性。 一個過度約束的 require 可能使規則因為沒有輸入能存活而空洞地通過。始終執行 --rule_sanity basic（偏好 advanced）。
• 樂觀標誌是不健全的。 --optimistic_loop、--optimistic_hashing、--optimistic_fallback 等會假設掉一些情況。請謹慎使用，記錄原因，並優先消除對它們的需求。
• 偏好 preserved 而非 filtered。 對於不變量，在 preserved 區塊（使用 requireInvariant）中編碼假設，而不是默默地排除方法。
• 使用 mathint 作為累加器。 uint256 中的求和與計數器可能溢出並產生幻影反例（或隱藏真實反例）；在無界 mathint 中計算，在邊界處進行型別轉換。
• 通過的規則強度完全取決於其假設。 每個摘要、連結、循環邊界和 require 都是證明中的漏洞。進行突變測試以確認規則能夠實際失敗。

---

最常用的檔案： 從 references/spec-patterns-cookbook.md 開始尋找正確配方，以及 examples/ERC20.spec 獲得一個完整的可調整工作規格。