zakrad/certora-prover-skill

Certora Prover（CVL / EVM）

Certora Prover 对智能合约进行形式化验证：你使用 CVL（Certora 验证语言）编写描述属性（规则和不变式）的 规范，验证器要么针对 所有 输入和状态 证明 它们，要么返回一个具体的 反例（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）断言某个基本属性在任何函数之后成立，仅用于确认测试工具能编译和运行。（→ references/rules-invariants.md，references/spec-patterns-cookbook.md）
4. 运行。 certoraRun MyContract.conf（或直接传递 .sol/.spec），然后打开报告链接。（→ references/running-and-config.md）
5. 阅读报告。 检查 CEX 调用轨迹和存储；修复规范或确认真正的 bug。（→ 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 确认你的规则确实能捕获注入的 bug——能通过突变的规范过度假设了。（→ references/debugging-and-timeouts.md）

10 秒快速入门

pip install certora-cli
export CERTORAKEY=<your-key>

// 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 与 assert 与 satisfy 与 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 与 Halmos 与 Foundry（不变式/模糊）与 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 — 当 需要一个完整的工作规范时阅读：方法块、余额之和幽灵+钩子、供应不变式、参数化/完整性/回滚/加性规则，以及铸造访问控制。
• 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 中的求和和计数器可能溢出，产生幻影 CEX（或隐藏真实 CEX）；在无界 mathint 中计算，在边界处强制转换。
• 通过规则仅与其假设一样强。 每个摘要、链接、循环边界和 require 都是证明中的一个漏洞。进行突变测试以确认规则实际能失败。

---

最常用文件： 从 references/spec-patterns-cookbook.md 获取正确配方，从 examples/ERC20.spec 获取完整的工作规范以便适配。