Certora 中的不变量介绍

Certora 的形式化验证

Certora 中不变量的介绍

模块 2：不变量、存储Hook、幽灵变量和代币的形式化验证

上次更新时间：2026 年 2 月 13 日

到目前为止，我们一直专注于验证单个方法或方法序列的行为——确保在给定特定输入的情况下，特定的函数调用或一组调用能够产生正确的状态变化。但验证还有另一个更普遍的方面：不变量。

不变量是合约状态必须始终保持为真的条件，无论调用哪个函数或按什么顺序调用。如果任何执行——无论是直接的还是通过一系列调用——违反了不变量，则表明合约设计存在根本性缺陷，可能暴露漏洞或安全风险。

在本文中，我们将探讨如何使用 Certora 的 CVL 内置不变量构造来形式化指定和验证这些属性。

在 CVL 中定义不变量

CVL 的内置不变量构造是一种形式化规范机制，它允许开发人员定义必须在智能合约整个生命周期中保持为真的通用属性（不变量），即从构造函数执行开始到合约将来可能达到的任何状态。

CVL 中的不变量使用 invariant 关键字定义，后跟一个唯一的名称（标识符）、可选参数以及一个描述必须始终保持为真的条件的布尔表达式，如下所示：

Copyinvariant invariant_name(optional_parameter_1, optional_parameter_2, ...)
    boolean_expression_in_CVL;

如果其布尔表达式（在不变量中定义）在合约的每个可达状态和其所有参数的所有可能值下都评估为 true，则该不变量被认为是成立的并报告为已验证 (✅)。我们将在本章后面更详细地探讨不变量验证过程。

不变量与规则的区别

CVL 中的规则旨在检查特定属性在定义的场景中是否为真：从某个状态开始，执行某些操作，然后检查结果。

Copyrule check_balance_updates(env e) {

    // 1. 初始状态
    address user = e.msg.sender;
    uint initial_balance = balanceOf(user);

    // 2. 操作
    uint amount;
    deposit(amount); // 调用 deposit 函数

    // 3. 结果检查
    uint final_balance = balanceOf(user);
    assert final_balance == initial_balance + amount, "存款未正确更新余额";
}

换句话说，它回答了这个问题：“此特定操作（或操作序列）是否导致预期结果？”

与侧重于特定场景的规则不同，CVL 中的不变量表示一个条件，该条件在合约的每个可达状态中都必须始终为真，无论调用了哪些函数或按什么顺序调用。

下面是一个简单不变量的示例，它声明 count 的值永远不会变为负数：

Copyinvariant count_cannot_be_negative()
    count() >= 0;

简而言之，它回答了这个问题：“无论合约如何使用，这个基本属性是否普遍为真？”

何时使用不变量与规则

决定在 CVL 中使用规则还是不变量取决于我们旨在验证的属性的性质。

何时使用规则：验证特定场景

当你的目标是验证特定上下文或特定操作序列中的行为时，请选择规则。例如：

1. withdraw(amount) 函数应从调用者的余额中正确扣除 amount 并进行转账，但前提是 balanceOf(caller) >= amount。
2. 验证尝试 mint 超出最大供应上限的操作是否正确回滚。
3. 检查管理功能是否只能由指定的管理员地址成功调用。

本质上，规则是你回答以下问题的首选方式：“此函数（或函数序列）在此特定情况下是否正常工作？”

何时使用不变量：强制执行基本真理

当你想验证一个必须在每个可能状态和每个可能的函数调用序列中都保持为真的属性时，请选择不变量。例如：

1. 在 ERC-20 实现中，totalSupply 必须始终等于所有单个用户余额的总和。
2. 在借贷协议中，假设清算正常运行，抵押品的总价值必须始终大于或等于总债务的某个百分比。
3. 在代币合约中，用户的余额永远不能变为负数。

不变量为你合约状态的长期完整性和安全性提供了最强的保证。它们回答了关键问题：“无论发生什么，我的合约的这个基本属性是否牢不可破？”

验证范围：规则 与 不变量

验证规则时，证明器会检查断言是否对规则中定义的特定场景（基于初始状态、执行的操作和任何假设）成立。规则为探索自定义路径或边缘情况提供了灵活性，但它们只验证规范中明确构建的执行路径的正确性。

相比之下，不变量必须成立，无论调用了哪些函数、带有何种参数或以何种顺序。证明器必须确保不变量在合约的每个可达状态中都得以维持。这是通过基于数学归纳法的两部分证明原则实现的：

1. 基本情况： 属性必须在合约部署后立即成立——即它必须由构造函数建立。
2. 归纳步骤： 对于合约中的每个公共或外部函数，如果属性在函数调用之前成立，则在函数调用之后也必须成立。

如果基本情况和归纳步骤都得到证明，则证明器将不变量报告为已验证 (✅)。

在 Certora 中编写不变量

为了理解不变量验证在实践中是如何工作的，让我们看看 Certora 文档中的简单 Voting 合约：

Copy// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

/// @title 一个简单的投票合约
contract Voting {

    // `hasVoted[user]` 为 true 如果用户已投票。
    mapping(address => bool) public hasVoted;

    uint256 public votesInFavor;  // 记录赞成票数

    uint256 public votesAgainst;  // 记录反对票数
    uint256 public totalVotes;    // 记录总投票数

    /// @notice 允许用户投票赞成提案。
    function voteInFavor() external {
        // 确保用户尚未投票
        require(!hasVoted[msg.sender], "你已经投过票了。");
        hasVoted[msg.sender] = true;

        votesInFavor += 1;
        totalVotes += 1;
    }

    /// @notice 允许用户投票反对提案。
    function voteAgainst() external {
        // 确保用户尚未投票
        require(!hasVoted[msg.sender], "你已经投过票了。");
        hasVoted[msg.sender] = true;

        votesAgainst += 1;
        totalVotes += 1;
    }
}

上面的 Voting 合约允许用户对提案投一票，要么赞成要么反对。为了防止重复投票，合约使用 hasVoted 映射来记录地址是否已经参与。它通过三个独立的计数器跟踪投票：votesInFavor、votesAgainst 和 totalVotes。当用户使用 voteInFavor() 或 voteAgainst() 函数投票时，相应的计数器会增加，hasVoted 状态会更新。

识别 Voting 合约中的关键不变量

由于我们旨在形式化验证 Voting 合约的不变量，我们首先需要识别其关键属性。查看我们的 Voting 合约，其中一个关键的不变量是总票数应始终等于赞成票数和反对票数之和。

识别出这个关键不变量后，让我们逐步了解使用 Certora 形式化指定和验证它的过程。

设置你的项目环境

要开始验证我们的不变量，我们首先需要设置项目结构和环境。为此，请按照以下说明操作：

1. 创建一个名为 certora-invariants-examples 的空目录，然后导航到该目录。

2. 在你的项目目录中，通过运行以下命令为项目创建 Python 虚拟环境。

   Copyvirtualenv certora-env

3. 通过运行以下命令激活你创建的 Python 虚拟环境。

   Copysource certora-env/bin/activate

4. 运行以下命令在你的虚拟环境中安装 Certora-CLI。

   Copypip3 install certora-cli

5. 运行以下命令在你的虚拟环境中安装 solc-select。

   Copypip3 install solc-select

6. 在你的项目目录中，创建三个子目录，分别命名为 contracts、specs 和 confs。

7. 在你的项目目录中，导航到 contracts 子文件夹并创建一个名为 Voting.sol 的文件。然后，将上面讨论的 Voting 合约粘贴到该文件中。

在规范文件中定义不变量

项目环境准备好后，下一步是创建一个规范文件，我们将在其中定义不变量。

1. 创建一个规范文件： 在你的项目目录中，导航到 specs 子文件夹并创建一个规范文件（例如，invariant.spec）。此文件将包含你的 CVL 规则，包括你想要验证的不变量。

2. 声明不变量： 在你的规范文件中，使用 invariant 关键字定义一个不变量。给它一个描述性名称，清楚地传达该规则检查的内容。

Copyinvariant totalVotesMatch()

3. 将不变量条件作为 CVL 表达式插入： 接下来，指定必须始终保持为真的条件。在 Voting 合约的情况下，我们希望确保总票数始终等于赞成票数和反对票数之和：

Copyinvariant totalVotesMatch()
  to_mathint(totalVotes()) == votesInFavor() + votesAgainst();

注意：to_mathint 用于将 Solidity 的 uint256 转换为 Certora 的数学整数以进行安全比较。无需将其应用于等式的右侧，因为在 CVL 中，所有算术运算的结果都会自动变为 mathint 类型。

4. 添加方法块： 接下来，让我们在规范顶部添加一个包含正确条目的方法块。

Copymethods {
    function totalVotes() external returns(uint256);
    function votesInFavor() external returns(uint256);
    function votesAgainst() external returns(uint256);
}

invariant totalVotesMatch()
    to_mathint(totalVotes()) == votesInFavor() + votesAgainst();

将函数声明为 envfree：由于 getter 函数 votesInFavor()、votesAgainst() 和 totalVotes() 不依赖于执行环境（即它们不读取 msg.sender、msg.value 或任何其他全局变量），我们可以将它们声明为 envfree。

Copymethods {
    function totalVotes() external returns(uint256) envfree;
    function votesAgainst() external returns(uint256) envfree;
    function votesInFavor() external returns(uint256) envfree;
}

invariant totalVotesMatch()
    to_mathint(totalVotes()) == votesInFavor() + votesAgainst();

运行验证

正确设置项目目录后，请按照以下步骤运行 Certora 证明器并验证你的不变量。

1. 创建配置文件： 在 confs 子文件夹中，创建一个配置文件（例如，invariant.conf）并将以下代码粘贴到其中。

Copy{
    "files": [\
        "contracts/Voting.sol:Voting"\
    ],
    "verify": "Voting:specs/invariant.spec",
    "msg": "Testing Invariant"
}

2. 添加 Certora 个人访问密钥： 在你的项目目录中，创建一个 .profile、.bashrc 或 .zshenv 文件（取决于你的操作系统和 shell）并添加以下行以将你的 Certora 个人访问密钥设置为环境变量。

Copy# Certora 访问密钥
export CERTORAKEY=<在此处添加你的 Certora 访问密钥>

3. 加载环境变量： 添加密钥后，通过运行下面显示的相应命令将环境变量加载到当前终端会话中。

Copy# 对于 bash 用户
source .profile

## 对于 zsh 用户
source .zshenv

4. 添加 Solidity 编译器： 在运行证明器之前，我们需要添加正确的 Solidity 编译器。要添加和使用正确的 Solidity 编译器版本，请运行以下命令。

Copysolc-select install 0.8.25
solc-select use 0.8.25

5. 运行证明器： 要验证你的不变量，请从项目根目录运行以下命令。

CopycertoraRun confs/invariant.conf

如果证明器成功编译你的智能合约和规范文件——没有遇到任何语法或语义错误，它将生成指向验证报告的链接并将其打印在你的终端输出中。

要查看验证结果，请使用浏览器打开终端中打印的链接。结果应与下图类似：

_注意：_根据你的规范复杂性和当前证明器队列情况，你的作业状态从“排队中”（Queued）变为“已执行”（Executed）可能需要几分钟。这种延迟是正常的，所以请不必担心。

上面显示的验证结果确认证明器已成功验证我们的不变量。这意味着，根据分析，没有发现任何可能破坏不变量的场景，这表明它在合约的整个行为中始终保持一致。

为了更好地理解不变量“成功验证”的含义，让我们检查证明器在幕后是如何验证不变量的。

不变量是如何被验证的？

当不变量提交进行验证时，证明器会执行两个必要的检查以确保其正确性，这直接对应于前面讨论的两部分证明原则（基于数学归纳法）：

• 初始状态检查： 首先，证明器验证不变量在合约的构造函数执行完成后立即成立。这是我们归纳证明的基本情况。
• 归纳步骤： 接下来，证明器检查每个公共和外部方法在其执行过程中是否保持不变量。这对应于归纳步骤，确保如果属性在函数调用之前成立，则在函数调用之后继续成立。

这两个检查的结果都可以通过展开证明器用户界面左侧面板中的不变量 totalVotesMatch() 来查看。

初始状态检查的结果显示在“归纳基础：构造函数之后”下，确认合约以不变量成立的有效状态开始。

归纳步骤的结果显示在“归纳步骤：外部（非视图）方法之后”下。证明的这一部分旨在表明所有公共和外部函数都保持不变量。

那么，为什么报告只显示“非视图”（状态改变）方法呢？

这是证明器的一个巧妙优化。Solidity 编译器保证 view 和 pure 函数不会改变合约的状态。逻辑如下：

1. 我们假设不变量在任何函数调用之前成立（归纳假设）。
2. 调用了一个视图函数。
3. 由于合约的状态保持不变，因此不变量在调用之后也必须成立。

因为 view 和 pure 函数永远不会改变合约的状态，所以在归纳步骤中无需再次验证它们。它们的正确性已通过归纳基础检查确保，该检查确认合约以有效状态开始。跳过这些冗余检查有助于证明器节省验证资源并消除报告中不必要的混乱。

因此，归纳步骤检查侧重于可以改变状态的方法。

在我们的例子中，voteAgainst() 和 voteInFavor() 都通过此检查进行分析。每个函数旁边的绿色对勾 (✅) 表示，当调用这些方法时，它们不会违反不变量。这证实了合约的逻辑在所有状态改变操作中都正确地保持了不变量。

除了这两个核心检查之外，证明器还会运行一个名为 envFreeFuncsStaticCheck 的规则，该规则验证规范中标记为 envfree 的所有函数是否真正独立于执行环境，例如 msg.sender 或 msg.value。

理解证明器用户界面中的附加检查

如果你使用的是 Certora 证明器的新版本，你可能会注意到在证明器用户界面中展开不变量结果时会出现额外的条目，例如 rule_not_vacuous 和 invariant_not_trivial_postcondition，如下图所示：

这些额外的条目是证明器自身添加的自动健全性检查。它们不是你编写的，也不意味着正在验证额外的不变量或规则。它们的目的是确保你的不变量真正有意义且不会轻易满足。

注意： 从 Certora 证明器 v8.1.0 开始，基本健全性检查默认运行（相当于设置 "rule_sanity": "basic"）。以前，默认是 "none"。你可以使用 --rule_sanity CLI 选项或通过在配置文件中添加 "rule_sanity": "none" 来禁用这些检查以控制此行为。有关所有可用健全性检查的详细说明，请参阅规则健全性检查文档。

这些检查验证了什么：

• rule_not_vacuous：确认不变量在实际条件下正在被评估。“空洞的”（vacuous）结果意味着不变量通过仅仅是因为前置条件从未满足——本质上，它从未真正被测试过。
• invariant_not_trivial_postcondition：确保不变量的条件并非无论合约状态如何都轻易为真（例如，一个总是评估为 true 的表达式）。

这些附加检查不会改变核心验证过程。证明器仍然执行相同的两部分归纳证明：验证不变量在构造函数之后成立（基本情况），以及每个状态改变函数都保持它（归纳步骤）。健全性检查只是提供了额外的信心，表明你的验证结果是有意义的，而不是规范错误的产物。

结论

智能合约不变量是关于合约状态的关键断言，它们必须始终保持为真。形式化验证这些不变量可确保合约在所有可能的状态和方法执行中保持其预期行为和正确性。

本文是关于 使用 Certora 证明器进行形式化验证 系列文章的一部分。

• 原文链接： rareskills.io/post/certo...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～