在 Certora 中测试 Revert 调用

形式化验证与 Certora

在 Certora 中测试 Revert 调用

模块 1：规则和基本 CVL 语法规则和基本 CVL 语法

最后更新于 2026 年 2 月 13 日

在本章中，我们将学习如何使用方法标签（@withrevert 和 @norevert）以及 CVL 中的特殊变量 lastReverted 来验证智能合约执行中的预期 revert。

为 Add() 函数设置验证场景

考虑以下 Math 合约，它有一个基本的 add() 函数，该函数接受两个无符号整数作为输入，并返回它们的和作为输出。

//SPDX-许可证标识符 : MIT
pragma solidity 0.8.25;

contract Math {

    function add(uint256 x, uint256 y) public pure returns (uint256) {
        return x + y;
    }

}

add() 函数的行为如下：

1. 提供有效输入时，它应正确计算 $x$ 和 $y$ 的和，并以 uint256 值返回结果。例如，add(15, 10) 将返回 25。
2. 由于合约使用 Solidity 0.8.0 或更高版本，如果和超过 uint256 的最大值（$2^{256} - 1$），交易将 revert。例如，如果 $x = 2^{256} - 1$ 且 $y = 1$，溢出将导致交易 revert 而不是返回结果。

验证 add() 函数规范

考虑以下规范来验证 Math 合约中 add() 函数的正确性：

methods {
    function add(uint256,uint256) external returns(uint256) envfree;
}

rule checkAdd() {

    uint256 a;
    uint256 b;
    uint256 c = add(a,b);

    assert a + b == c;
}

要查看上述规范的验证结果，运行 Prover 并打开验证链接，将看到类似下图的结果。

这可能令人惊讶，因为当 x 和 y 的和超过 uint256 的最大值时，add() 函数预期会 revert。由于 Prover 探索不同的执行路径来验证正确性，人们会期望它也遇到 revert 场景。在这种情况下，assert 语句应该评估为 false，并且规则应该验证失败。

然而，这并没有发生，我们的规则仍然通过了 Prover 的验证。这是因为，默认情况下，Prover 在验证过程中会忽略 revert 情况。

这引出了一个重要问题：为什么 Prover 在验证过程中选择忽略 revert 情况？

为什么 Prover 忽略 Revert 路径？

原因是 revert 可能是操作的正常部分——例如，如果合约所有者之外的某人试图执行特权操作。在这种情况下，revert 不被视为失败；它是预期行为。

通过忽略 revert 路径，Prover 专注于验证函数成功执行且没有错误的情况。但是，我们可以使用 CVL 提供的 @withrevert 方法标签来覆盖此默认行为。

CVL 方法标签介绍

Certora 为我们提供了两个方法标签，@norevert 和 @withrevert，它们可以放在方法名之后，但在方法参数之前，如下所示：

function_name@norevert();
function_name@withrevert();

当我们使用 @norevert 标签进行方法调用时，Prover 会主动忽略任何导致 revert 的执行路径。换句话说，function_name@norevert() 的行为与 function_name() 完全相同。

另一方面，当我们使用 @withrevert 标签进行方法调用时，Prover 不再忽略 revert 情况。相反，它将任何发生 revert 的场景视为违规。例如，考虑下面带有 @withrevert 标签的 checkAdd() 规则：

methods {
    function add(uint256,uint256) external returns(uint256) envfree;
}

rule checkAdd() {

    uint256 a;
    uint256 b;

    uint256 c = add@withrevert(a,b);

    assert a + b == c;
}

当我们使用此更新的规范重新运行 Prover 时，结果发生了变化：规则现在验证失败，如下图所示：

由于我们在 add() 函数调用中使用了 @withrevert 标签，Prover 不再忽略 revert 情况。因此，如果 $a$ 和 $b$ 的和超过 uint256 的最大值，规则会将 revert 视为违规。验证器检测到此问题并报告一个反例——一个导致溢出和 revert 的反例，最终导致断言失败。当发生 revert 时，没有返回值——$c$ 不受约束，可以取任意值。因此，断言 $a + b == c$ 无法成立。

引入 CVL 特殊变量：lastReverted

在 CVL 中，我们可以访问一个特殊的布尔变量 lastReverted，它在每次方法调用后更新——包括那些没有使用 @withrevert 进行的调用。该变量指示最近的合约函数是 revert（$lastReverted = \text{true}$）还是成功执行（$lastReverted = \text{false}$）。

然而，默认情况下，Prover 会忽略任何会导致 revert 的执行路径。这意味着，当函数在没有 @withrevert 的情况下被调用时——例如使用默认调用或 @norevert 标签时——Prover 不会探索 revert 场景，lastReverted 的值将始终保持为 false。

为了准确跟踪函数是否 revert，我们必须明确指示 Prover 使用 @withrevert 标签考虑 revert 路径。当函数使用 @withrevert 调用时，Prover 不再忽略 revert 场景，如果发生 revert，$lastReverted$ 将更新为 $\text{true}$。

示例：检测因溢出导致的 Revert

现在，让我们看看如何在实际验证规则中使用 lastReverted。我们将测试 add() 函数，确保它在发生溢出和不发生溢出的情况下都能正确运行。

情况 1：函数在溢出时应 Revert

考虑下面的 addShouldRevert() 规则，它旨在验证 add() 函数在发生溢出时是否正确 revert。

methods {
    function add(uint256,uint256) external returns(uint256) envfree;
}

rule addShouldRevert() {

    uint256 a;
    uint256 b;

    require(a + b > max_uint256);

    add@withrevert(a,b);

    assert lastReverted; // 这等同于 assert lastReverted == true;
}

addShouldRevert() 规则中的语句 require($a + b > \text{max\_uint256}$); 确保输入的 $a$ 和 $b$ 的选择方式使得它们的和超过 uint256 可以存储的最大值，从而导致溢出。Solidity 的算术运算在溢出情况下会自动 revert，触发 add(a, b) 函数调用的 revert。

注意：在 CVL 中，不同整数类型的最大值作为变量可用，例如 max_uint8, max_uint16, …, max_uint256, 等。

由于该函数是使用 @withrevert 调用的，Prover 不会忽略 此 revert 场景并正确检测到它。结果，$lastReverted$ 被设置为 $\text{true}$，表示函数执行已 revert。断言 assert lastReverted; 然后评估为 true，因为 $lastReverted$ 与预期结果匹配。因此，该规则应该通过，如下图所示。

情况 2：函数在有效加法时不应 Revert

同样，考虑 addShouldNotRevert() 规则，它旨在验证当 $a$ 和 $b$ 的和保持在有效 uint256 范围内时，add() 函数不会 revert。

methods {
    function add(uint256,uint256) external returns(uint256) envfree;
}

rule addShouldNotRevert() {

    uint256 a;
    uint256 b;

    require(a + b <= max_uint256);

    add@withrevert(a,b);

    assert !lastReverted;
}

在上述规则中，语句 require($a + b \le \text{max\_uint256}$); 确保输入的 $a$ 和 $b$ 的选择方式使得它们的和不会导致溢出。由于 Solidity 的算术运算仅在溢出或其他显式失败发生时才 revert，因此 add(a, b) 函数成功执行而不会 revert。

由于该函数是使用 @withrevert 调用的，Prover 会跟踪是否发生 revert。然而，由于加法没有超过 uint256 限制，所以没有发生 revert，$lastReverted$ 保持为 $\text{false}$。断言 assert $\text{!lastReverted}$; 验证了这一点，确保规则成功通过，如下图所示。

避免 lastReverted 被覆盖

由于 lastReverted 在每次函数调用后都会更新，随后的调用可能会覆盖其值。这意味着如果一个函数 revert，但另一个函数紧接着执行，原始的 revert 状态将丢失。

为防止验证错误，请始终在相关函数调用之后立即捕获 lastReverted，然后再进行可能覆盖其值的其他调用。

为了说明这一点，我们来看一个简单的算术合约：

// SPDX-许可证标识符: MIT
pragma solidity 0.8.25;

contract Math {

    function add(uint256 x, uint256 y) public pure returns (uint256) {
        return x + y;
    }

    function divide(uint256 x, uint256 y) public pure returns (uint256) {
        return x / y;
    }
}

上述合约定义了两个基本函数：

• add($x$, $y$) 简单地返回 $x$ 和 $y$ 的和。
• divide($x$, $y$) 执行整数除法，如果 $y == 0$，由于 Solidity 内置的除零保护，它会revert。

现在，考虑以下规则，旨在验证当接收 0 作为第二个参数时，这两个函数的行为：

methods {
    function divide(uint256,uint256) external returns(uint256) envfree;
    function add(uint256,uint256) external returns(uint256) envfree;
}

rule checkMath() {

    uint256 a;

    divide@withrevert(a,0);
    bool divideCallStatus = lastReverted;

    add@withrevert(a,0);
    bool addCallStatus = lastReverted;

    assert divideCallStatus == true;
    assert addCallStatus == false;
}

如果我们不立即存储 lastReverted 在调用 divide(a, 0) 之后，下一个函数调用（add(a, 0)）将再次更新它，完全抹去关于除法操作失败的信息。

这意味着如果一个规则稍后检查 divide(a, 0) 是否 revert，它可能会错误地得出结论，认为函数执行成功了——即使它实际上失败了。这种错误的验证可能导致不正确的合约分析，从而引发安全漏洞或关键逻辑中的错误假设。

通过在调用 divide(a, 0) 之后立即存储 lastReverted，我们确保在进行任何其他调用之前准确捕获函数行为。这保留了正确的执行历史，防止意外覆盖并确保可靠验证。

总结

测试成功和 revert 两种情况对于方法的形式化验证至关重要，因为它可以提供更好的覆盖范围，并确保方法在所有可能的输入条件下（包括溢出或无效输入等边缘情况）都能正确运行。

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

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