ERC-721 的铸造和销毁规则

聚焦于使用 Certora Prover 对 ERC-721 代币的铸造和销毁操作进行形式化验证。文章详细剖析了 CVL 规则的构建，包括如何设定前置条件、记录状态、处理函数调用及通过存活、影响和无副作用断言来确保智能合约的正确性和安全性。

Certora 形式化验证

ERC-721 的铸造和销毁规则

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

最后更新于 2026 年 2 月 13 日

介绍

ERC-721 是以太坊非同质化代币（NFT）的标准，广泛用于代表数字财产。像任何形式的财产一样，它围绕着供应的创建、供应的移除和所有权的转移。

本章重点介绍对铸造（mint）和销毁（burn）操作进行形式化验证。这是 OpenZeppelin 的 ERC-721 CVL 规范代码演练的第一部分 (1/5)。

OpenZeppelin 在其规范中使用了将三种断言类型组合到一个规则中的模式，分类如下：

  1. 活性（Liveness）—— 指定函数在不回滚的条件。
  2. 效果（Effect）—— 指定函数未回滚时发生的状态变化。
  3. 无副作用（No side-effect）—— 指定除了效果断言中的状态变化外，没有发生意外的状态变化。

暴露内部函数 _mint() 和 _burn() 用于验证

_mint() 和 _burn() 是内部函数，旨在供开发者继承并构建用于创建和销毁 NFT 的自定义逻辑。在此规范中，辅助合约（harness contract）继承并将其暴露为外部函数，这允许 Prover 在验证期间调用 _mint() 和 _burn()。

以下是 OpenZeppelin 的实现：

  • _mint()
  • _burn()
  • 暴露它们的辅助合约
// ERC721.sol

function _mint(address to, uint256 tokenId) internal {
    if (to == address(0)) {
        revert ERC721InvalidReceiver(address(0));
    }
    address previousOwner = _update(to, tokenId, address(0));
    if (previousOwner != address(0)) {
        revert ERC721InvalidSender(address(0));
    }
}
...

function _burn(uint256 tokenId) internal {
    address previousOwner = _update(address(0), tokenId, address(0));
    if (previousOwner == address(0)) {
        revert ERC721NonexistentToken(tokenId);
    }
}
// ERC721Harness.sol

function mint(address account, uint256 tokenId) external {
    _mint(account, tokenId);
}
...

function burn(uint256 tokenId) external {
    _burn(tokenId);
}

形式化验证铸造

mint() 操作创建新代币并将其分配给接收者。我们形式化验证：

  • 当且仅当代币未被铸造且接收者有效时，它才不会回滚。
  • 如果它不回滚，则总供应量和接收者的余额都增加一。
  • 接收者成为所有者。
  • 没有其他账户余额或代币所有权发生变化。

以下是证明这些属性的 CVL 规则：

// ERC721.spec -- mint (explanation follows)

rule mint(env e, address to, uint256 tokenId) {
    // preconditions
    require nonpayable(e);
    // requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);

    // pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

    // method call
    mint@withrevert(e, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

    // no side effect
    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
}

我们将按以下方式讨论上述规则的各个部分：

  • 前置条件（Preconditions）
  • 调用前状态（Pre-call state）
  • 铸造调用（Mint call）
  • 断言（Assertions）
    • 活性（liveness）
    • 效果（effect）
    • 无副作用（no side-effect）

前置条件

前置条件是规则中的一个约束，指定在 Prover 执行 mint() 方法之前必须为真。它可能在调用“之后”仍然成立，也可能不成立，具体取决于方法引起的状态变化。

以下是 mint 规则的前置条件：

require nonpayable(e);
// requireInvariant notMintedUnset(tokenId); // intentionally commented out
...

require balanceLimited(to);

注意：为了简化讨论，不变量前置条件 notMintedUnset(tokenId) 被注释掉了，因为 mint 规则没有它也能成功验证。我们将在下一章介绍 ERC-721 代码库的 CVL 不变量。

  • require nonpayable(e)

这要求调用时不发送任何 ETH，因为 mint() 是不可支付的。nonpayable(e) 被表示为一个 definition，如果 $e.msg.value == 0$ 则返回 true，否则返回 false：

definition nonpayable(env e) returns bool = e.msg.value == 0;

它通过将条件 $e.msg.value == 0$ 绑定到一个名为 nonpayable(e) 的可重用表达式，封装了检查调用是否不携带 ETH 的逻辑。这个定义允许我们在整个规范中引用该条件，而不是每次调用不可支付函数时都重复编写 $e.msg.value == 0$。

注意： definition 在 CVL 中是一个广泛的话题。有关更多信息，请查阅 Certora 文档 。在本系列中，定义被直接用作可重用表达式以提高代码可读性。

  • require balanceLimited(to)

这要求接收者的余额小于 $max\_uint256$。它也被表示为一个 definition，如果 $balanceOf(account) < max\_uint256$ 则返回 true：

definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

OpenZeppelin ERC-721 实现为了节省 gas，有意在 unchecked 代码块中增加余额。溢出在理论上是可能的，但在实践中不可能，因为达到 $max\_uint256$ 需要铸造比实际可能存在的更多的 NFT。因此，前置条件 require $balanceLimited(to)$ 是合理的。

如果没有前置条件 $balanceLimited(to)$，Prover 将会考虑溢出情况，因为 mint() 调用了 _update() 函数，其中余额增加发生在 unchecked 代码块中：

// ERC721.sol

function _mint(address to, uint256 tokenId) internal {
      ...
      address previousOwner = _update(to, tokenId, address(0));
      ...
}
/// ERC721.sol

function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
      ...

      if (to != address(0)) {
          unchecked {
              _balances[to] += 1;
          }
      }
      ...
}

记录调用前状态——铸造调用前的总供应量、余额和所有权

在调用 mint() 函数之前，记录以下状态。然后将这些值与断言部分中的调用后值进行比较：

mathint supplyBefore         = _supply;
uint256 balanceOfToBefore    = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore          = unsafeOwnerOf(tokenId);
address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
  • $mathint supplyBefore = _supply$

这记录了铸造调用前的总供应量，以便与铸造后的供应量进行比较，并确认其增加了 $1$。

$_supply$ 是一个幽灵变量（ghost variable），它通过 Sstore Hook跟踪总供应量，并在添加新余额和减去旧余额时进行更新。

幽灵变量 $_supply$ 被声明为 $mathint$ 类型，因此 $supplyBefore$ 也必须是 $mathint$ 类型。如果 $supplyBefore$ 被声明为 $uint256$ 类型，Prover 将报告类型错误。这个错误出现是因为 $mathint$ 表示一个无界的数学整数，而 $uint256$ 表示一个有界整数。将 $mathint$ 值赋给 $uint256$ 将假定该值适合 $256$ 位，这是 Prover 无法安全假定的。

以下是更新幽灵变量 $_supply$ 的 Sstore Hook实现：

ghost mathint _supply {
      init_state axiom _supply == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
      _supply = _supply - oldValue + newValue;
}
  • $uint256 balanceOfToBefore = balanceOf(to)$

这记录了铸造调用前接收者的余额，以便与铸造后的余额进行比较，并确认其也增加了 $1$。

  • uint256 balanceOfOtherBefore = balanceOf(otherAccount)

这记录了铸造调用前任何其他账户的余额，以便与铸造后的余额进行比较，并确认其未发生变化，因此没有副作用。

  • address ownerBefore = unsafeOwnerOf(tokenId)

这记录了铸造调用前代币的拥有者。为了铸造成功，该值必须为零，这是活性条件之一（$ownerBefore == 0$ 和 $to != 0$）。

unsafeOwnerOf() 是一个辅助函数（harness function），即使对于没有有效所有者的代币，它也能暴露所有权。对于未铸造的代币，它返回零地址，这与 ownerOf() 不同，后者在这种情况下会回滚。这使得该规则能够比较铸造前后的所有权，因为这些所有权转换涉及零地址（未铸造状态）到有效所有者地址。

  • address otherOwnerBefore = unsafeOwnerOf(otherTokenId)

这记录了在铸造调用之前，任意其他代币（不是正在铸造的那个）的拥有者，这样我们就可以确认它在铸造后没有改变，因此没有副作用。

铸造调用

@withrevert 标签允许 Prover 探索回滚和不回滚的路径。!lastReverted 条件捕获了调用是否没有回滚，并将其存储为 success：

mint@withrevert(e, to, tokenId);
bool success = !lastReverted;

断言——活性、效果和无副作用

如前所述，整个规范中使用的规则模式将活性、效果和无副作用组合到单个规则中。以下是我们将详细解释的代码块：

// liveness
assert success <=> (
    ownerBefore == 0 &&
    to != 0
);

// effect
assert success => (
    _supply                   == supplyBefore + 1 &&
    to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
    unsafeOwnerOf(tokenId)    == to
);

// no side effect
assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;

活性（Liveness）：

下面的断言表明 _mint() 当且仅当代币未被铸造（$ownerBefore == 0$）并且接收者有效（$to != 0$）时才不会回滚：

// liveness
assert success <=> (
    ownerBefore == 0 &&
    to != 0
);

我们在前两章中使用了回滚和析取模式。如果我们将上述断言转换为该模式，它将变为：

_mint() 当且仅当代币已被铸造（$ownerBefore != 0$）或接收者无效（$to == 0$）时才会回滚。

// reverts
assert !success <=> (
    ownerBefore != 0 ||
    to == 0
);

“成功 + 合取”模式（活性）列出了函数成功的所有条件，而“回滚 + 析取”模式列出了函数回滚的所有条件。它们在逻辑上是等价的。

效果（Effect）：

如果 mint() 函数没有回滚，那么产生的状态变化是：

  • 总供应量恰好增加一（$_supply == supplyBefore + 1$）
  • 接收者的余额恰好增加一（$balanceOf(to) == balanceOfToBefore + 1$）
  • 代币现在归接收者所有（$unsafeOwnerOf(tokenId) == to$）
// effect
assert success => (
    _supply                   == supplyBefore + 1 &&
    to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
    unsafeOwnerOf(tokenId)    == to
);

无副作用（No side effect）：

以下断言检查 mint() 函数没有引起意外的副作用：

  • assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to

    这检查只有目标接收者的余额发生变化，所有其他账户不受影响。如果一个账户的余额在铸造调用后发生变化，那么该账户就是接收者（to）。如果一个账户的余额没有变化，那么该账户不是接收者，因此不受铸造调用的影响。

  • assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId

    这检查只有被铸造代币的所有者发生变化，所有其他代币不受影响。如果一个代币的所有者在铸造调用后发生变化，那么该代币就是被铸造的代币。如果一个代币的所有者没有变化，那么该代币不是被铸造的代币，因此其所有权不受铸造调用的影响。

// no side effect
assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;

现在，这是完整的规范，其中包括 mint 规则、定义、幽灵变量和Hook：

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mathint _supply {
    init_state axiom _supply == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
    _supply = _supply - oldValue + newValue;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: mint behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule mint(env e, address to, uint256 tokenId) {
    require nonpayable(e);
    // requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);

    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

    mint@withrevert(e, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

    // no side effect
    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
}

这是 Prover 运行结果。

形式化验证销毁

销毁操作执行与铸造相反的状态更改。

铸造时，状态变化是：

  • $_supply$ 增加 $1$
  • $balanceOf(to)$ 增加 $1$
  • $ownerOf(tokenId)$ 从之前的值 $address(0)$ 变为非零地址

销毁时，发生相反的情况：

  • $_supply$ 减少 $1$
  • $balanceOf(from)$ 减少 $1$
  • $ownerOf(tokenId)$ 从其之前的非零地址变回 $address(0)$

与铸造不同，铸造时新创建的代币没有现有的批准，销毁操作必须作为清除代币的一部分移除任何现有的批准。

考虑到这些行为，我们形式化验证：

  • 当且仅当代币存在（即所有者不是 $address(0)$）时，它才不会回滚。
  • 如果调用成功，总供应量减少一，之前所有者的余额减少一。
  • 所有者设置为 $address(0)$，这意味着代币没有所有者。
  • 代币批准被清除。
  • 没有其他账户余额、代币所有权或批准发生变化。

以下是证明这些属性的 CVL 规则：

// ERC721.spec -- burn (explanation follows)

rule burn(env e, uint256 tokenId) {
    // preconditions
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);

    // pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    // method call
    burn@withrevert(e, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

前置条件

与 mint 规则相同，此规则是不可支付的。因此，require nonpayable(e) 是必要的：

require nonpayable(e);
...

记录调用前状态——销毁调用前的总供应量、余额、所有权和批准

mint 规则中记录的所有调用前状态也出现在 burn 规则中，除了以下几点：

  • $uint256 balanceOfFromBefore = balanceOf(from)$

    销毁规则没有记录铸造接收者（$balanceOf(to)$）的调用前状态，而是记录了所有者（$balanceOf(from)$）的余额，以验证在销毁调用结束时，余额减少了 $1$。

  • address otherApprovalBefore = unsafeGetApproved(otherTokenId)

    批准在销毁函数中是必要的；因此，它记录了任意其他代币的批准，以验证其保持不变。

销毁调用

与之前的规则一样，调用使用了 @withrevert 标签。布尔变量 success 捕获了调用是否没有回滚（!lastReverted），这用于验证调用前和调用后状态之间的预期变化：

burn@withrevert(e, tokenId);
bool success = !lastReverted;

断言——活性、效果和无副作用

此处检索到的所有值均为调用后状态，并与调用前状态进行比较：

// liveness
assert success <=> (
    ownerBefore != 0
);

// effect
assert success => (
    unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
    to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
    unsafeOwnerOf(tokenId)      == 0 &&
    unsafeGetApproved(tokenId)  == 0
);

// no side effect
assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

活性（Liveness）：

它断言销毁调用当且仅当要销毁的 $tokenId$ 具有所有者时才不会回滚。

效果（Effect）：

如果销毁调用没有回滚，则意味着所有以下状态更改都必须已经发生：

  • $unsafeOwnerOf(tokenId) != 0 \Rightarrow (\_supply == supplyBefore - 1)$

    如果代币已铸造（拥有非零所有者），则供应量恰好减少 $1$。这意味着供应量的减少仅在至少有一个已铸造代币时才进行检查。

  • $to\_mathint(balanceOf(from)) == balanceOfFromBefore - 1$

    from 地址（代币所有者）的余额减少了 $1$。

  • $unsafeOwnerOf(tokenId) == 0$

    代币的所有权已被清除，因此 $unsafeOwnerOf(tokenId)$ 返回 $0$。

  • $unsafeGetApproved(tokenId) == 0$

    代币的任何现有批准已被移除，因此 $unsafeGetApproved(tokenId)$ 返回 $0$。

无副作用（No side effect）：

  • $balanceOf(otherAccount) != balanceOfOtherBefore \Rightarrow otherAccount == from$

    这检查只有销毁前的所有者余额发生变化，所有其他账户不受影响。如果一个账户的余额在销毁调用后发生变化，那么该账户就是销毁前的所有者。

  • $unsafeOwnerOf(otherTokenId) != otherOwnerBefore \Rightarrow otherTokenId == tokenId$

    这检查只有被销毁代币的所有权发生变化，所有其他代币不受影响。如果一个代币的所有者在销毁调用后发生变化，那么该代币就是被销毁的代币。

  • $unsafeGetApproved(otherTokenId) != otherApprovalBefore \Rightarrow otherTokenId == tokenId$

    这检查只有被销毁代币的批准被清除，所有其他代币的批准不受影响。如果一个代币的批准在销毁调用后发生变化，那么该代币就是被销毁的代币。

这是销毁规则的完整规范：

methods {
    function ownerOf(uint256) external returns (address) envfree;
    function balanceOf(address) external returns (uint256) envfree;

    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonpayable(env e) returns bool = e.msg.value == 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mathint _supply {
    init_state axiom _supply == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
    _supply = _supply - oldValue + newValue;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: burn behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule burn(env e, uint256 tokenId) {
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);

    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    burn@withrevert(e, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

注意：行 $requireInvariant ownerHasBalance(tokenId)$ 被注释掉了，因为 Prover 8.3.1 报告此不变量存在冲突，因此无法在此规范中应用。这导致“效果”断言从 $_supply == supplyBefore - 1$ 调整为 $unsafeOwnerOf(tokenId) != 0 \Rightarrow (\_supply == supplyBefore - 1)$ 。所有不变量，包括 $ownerHasBalance(tokenId)$ ，将在下一章讨论。

这是 burn 规则的 Prover 运行结果。

铸造和销毁的完整规范

这是完整的规范和 Prover 运行结果。

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

  • 原文链接： rareskills.io/post/certo...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
RareSkills
RareSkills
https://www.rareskills.io/

RareSkills

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！