⚡

Certora形式化验证器 certora-prover

Certora形式化验证技能是一种用于智能合约安全审计和数学证明的专业工具。通过CVL规范语言，提供不变式验证、参数化测试、幽灵变量跟踪和反例分析功能，确保区块链智能合约的正确性和安全性。关键词：智能合约安全、形式化验证、CVL语言、数学证明、区块链审计、DeFi安全、合约测试、反例分析、幽灵变量、参数化规则。

智能合约 0 次安装 0 次浏览 更新于 2/23/2026

name: certora-prover description: 使用Certora Prover进行形式化验证，采用CVL规范语言。支持不变式规则、参数化验证、幽灵变量和反例分析，为合约正确性提供数学证明。 allowed-tools: Read, Grep, Write, Bash, Edit, Glob, WebFetch

Certora 形式化验证技能

使用Certora Prover对智能合约进行形式化验证，提供合约正确性的数学证明。

能力

  • CVL规范：编写Certora验证语言规范
  • 不变式规则：定义和验证状态不变式
  • 参数化规则：编写全面的属性测试
  • 幽灵变量：跟踪抽象状态
  • 反例分析：分析验证失败案例
  • 循环处理：配置循环不变式和展开
  • 函数摘要：抽象复杂函数

安装

# 安装Java（必需）
sudo apt install openjdk-17-jdk

# 安装Certora CLI
pip install certora-cli

# 设置API密钥
export CERTORAKEY=<你的API密钥>

# 验证安装
certoraRun --version

项目设置

目录结构

项目/
├── 合约/
│   └── Token.sol
├── certora/
│   ├── 配置/
│   │   └── token.conf
│   └── 规范/
│       └── token.spec
└── foundry.toml

配置文件

# certora/配置/token.conf
{
  "files": ["合约/Token.sol"],
  "verify": "Token:certora/规范/token.spec",
  "solc": "solc-0.8.20",
  "msg": "Token验证",
  "rule_sanity": "basic",
  "optimistic_loop": true,
  "loop_iter": 3
}

CVL规范语言

基本规则

// certora/规范/token.spec

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
    function transfer(address, uint256) external returns (bool);
}

// 不变式：余额永不超过总供应量
invariant balanceUnderSupply(address user)
    balanceOf(user) <= totalSupply()

// 规则：转账保持总供应量不变
rule transferPreservesTotalSupply(address to, uint256 amount) {
    env e;

    uint256 supplyBefore = totalSupply();

    transfer(e, to, amount);

    uint256 supplyAfter = totalSupply();

    assert supplyBefore == supplyAfter,
        "转账后总供应量发生变化";
}

参数化规则

// 参数化规则：任何函数都保持不变式
rule anyFunctionPreservesInvariant(method f) {
    env e;
    calldataarg args;

    uint256 supplyBefore = totalSupply();

    f(e, args);

    uint256 supplyAfter = totalSupply();

    assert supplyBefore == supplyAfter,
        "总供应量发生变化";
}

幽灵变量

// 幽灵变量：跟踪所有余额总和
ghost mathint sumBalances {
    init_state axiom sumBalances == 0;
}

// 钩子：余额变化时更新幽灵变量
hook Sstore balances[KEY address user] uint256 newBalance
    (uint256 oldBalance) STORAGE {
    sumBalances = sumBalances + newBalance - oldBalance;
}

// 使用幽灵变量的不变式
invariant totalSupplyIsSumOfBalances()
    to_mathint(totalSupply()) == sumBalances

函数摘要

// 外部调用的摘要
methods {
    function _.transfer(address, uint256) external => DISPATCHER(true);
    function _.balanceOf(address) external returns (uint256) => DISPATCHER(true);
}

// 非确定性摘要
methods {
    function externalCall() external => HAVOC_ECF;
}

// 常量摘要
methods {
    function getConstant() external returns (uint256) => ALWAYS(100);
}

循环处理

// 循环不变式
rule loopInvariant() {
    env e;

    // 配置循环展开
    require e.msg.sender != 0;

    // 循环迭代次数由配置限制
    processArray(e);

    assert true; // 验证循环终止
}

运行验证

基本运行

# 运行验证
certoraRun certora/配置/token.conf

# 运行特定规则
certoraRun certora/配置/token.conf --rule transferPreservesTotalSupply

# 带消息运行
certoraRun certora/配置/token.conf --msg "PR #123 验证"

高级选项

# 完整性检查
certoraRun certora/配置/token.conf --rule_sanity basic

# 乐观循环处理
certoraRun certora/配置/token.conf --optimistic_loop --loop_iter 5

# 多合约验证
certoraRun 合约/Token.sol 合约/Staking.sol \
  --verify Token:规范/token.spec

# 调试模式
certoraRun certora/配置/token.conf --debug

结果解读

验证输出

规则: transferPreservesTotalSupply
  状态: 已验证 ✓
  时间: 45秒

规则: balanceUnderSupply
  状态: 违反 ✗
  反例:
    - 用户: 0x1234...
    - 初始余额: 100
    - 最终余额: 200
    - 总供应量: 150

反例分析

  1. 检查调用跟踪：理解调用序列
  2. 检查状态变化：跟踪存储修改
  3. 识别假设：检查假设是否太弱
  4. 验证模型：确保CVL规范符合意图

常见模式

ERC-20验证

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
    function allowance(address, address) external returns (uint256) envfree;
}

// 转账完整性
rule transferIntegrity(address to, uint256 amount) {
    env e;
    address from = e.msg.sender;

    uint256 fromBalanceBefore = balanceOf(from);
    uint256 toBalanceBefore = balanceOf(to);
    require from != to;

    transfer(e, to, amount);

    uint256 fromBalanceAfter = balanceOf(from);
    uint256 toBalanceAfter = balanceOf(to);

    assert fromBalanceAfter == fromBalanceBefore - amount;
    assert toBalanceAfter == toBalanceBefore + amount;
}

// 授权单调性
rule approveIntegrity(address spender, uint256 amount) {
    env e;

    approve(e, spender, amount);

    assert allowance(e.msg.sender, spender) == amount;
}

访问控制验证

methods {
    function owner() external returns (address) envfree;
    function setOwner(address) external;
}

// 只有所有者可以更改所有者
rule onlyOwnerCanChangeOwner(address newOwner) {
    env e;

    address ownerBefore = owner();

    setOwner(e, newOwner);

    assert e.msg.sender == ownerBefore,
        "非所有者更改了所有者";
}

CI/CD集成

GitHub Actions

name: Certora验证
on: [push, pull_request]

jobs:
  certora:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3

      - name: 安装Certora
        run: pip install certora-cli

      - name: 运行验证
        env:
          CERTORAKEY: ${{ secrets.CERTORAKEY }}
        run: certoraRun certora/配置/token.conf

流程集成

流程 目的
formal-verification.js 主要验证
smart-contract-security-audit.js 深度安全分析
lending-protocol.js 协议正确性
amm-pool-development.js DeFi不变式
governance-system.js 治理属性

最佳实践

  1. 从简单不变式开始
  2. 使用参数化规则进行全面覆盖
  3. 记录所有假设
  4. 仔细分析反例
  5. 使用幽灵变量进行复杂状态跟踪
  6. 设置适当的循环边界
  7. 在CI中运行夜间验证

另请参阅

  • skills/slither-analysis/SKILL.md - 静态分析
  • skills/echidna-fuzzer/SKILL.md - 属性模糊测试
  • agents/formal-methods/AGENT.md - 验证专家
  • Certora文档