用途：Certora 是面向智能合约的形式化验证工具，用 CVL（Certora Verification Language）编写规范，将 Solidity 与 CVL 翻译为 SMT 公式并穷尽验证，覆盖所有输入、调用序列与存储状态，而非随机采样或模糊测试。
主要能力：支持规则（rule）、不变量（invariant）、幽灵变量（ghost）、钩子（hook）、参数化规则（method f + calldataarg）、多合约验证、dispatcher、harness 等。assert 检查普遍性，satisfy 检查可达性；@withrevert 可验证回滚条件；mathint 为无界整数类型。规则失败时输出具体反例，含调用序列、存储值与变量赋值。
使用方式：安装 pip install certora-cli（需 Python 3.8.16+、Java 11+、solc 在 PATH）。设置环境变量 export CERTORAKEY="your-api-key-here"，用 certoraRun --version 验证。编写 .spec 与 .conf 文件后运行 certoraRun certora/Token.conf。配置项包括 files、verify、solc、optimistic_loop、loop_iter、rule_sanity、link、packages、smt_timeout 等。
适用场景：ERC-20 等代币合约、金库、权限控制等需要数学证明正确性的场景，尤其适合审计与 CI 集成。
限制：Prover 运行在 Certora 云端，需 API Key；学术与开源项目可免费使用，商业定价按验证分钟计费。CVL 与 Solidity 语法不同，不能使用 abi.encode、keccak256 等表达式。循环需显式设置 --loop_iter，默认 1 次，过高会显著增加验证时间。CVL 中的 require 约束证明器而非合约，过度约束会导致规则空洞通过，需用 rule_sanity 检测。不变量采用归纳法证明，preserved 块缺失假设常导致失败。具体平台支持与最新定价暂未提供。