形式化验证一个计数器

Certora 的形式化验证

形式化验证一个计数器

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

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

在上一章中，我们学习了形式化验证的理论方面，包括它是什么以及它是如何工作的。在本模块中，我们将超越理论，学习以下内容：

• 如何设置项目以使用 Certora Prover。
• 如何获取和使用 Certora 访问密钥。
• 如何使用 Certora Prover 执行形式化验证。

让我们首先设置 Certora Prover 的项目环境。

安装必要的先决条件工具

在设置项目目录之前，请确保你的本地机器已安装以下先决条件：

• Java Development Kit(JDK) 21 或更高版本

• Python 3.9 或更高版本

你可以通过在终端中运行 python3 --version 和 java --version 命令来检查你的机器是否已安装这两个软件。

💡 对于 Windows 用户，我们强烈建议使用适用于 Linux 的 Windows 子系统 (WSL) 以获得更好的体验。

设置我们的项目目录

安装完先决条件后，创建一个名为 certora-counter 的空目录，进入该目录，然后按照以下说明正确设置你的项目目录。

1. 在你的本地机器上，运行以下命令安装 virtualenv。这个工具将允许我们创建一个 Python 虚拟环境，这对于管理项目目录中的依赖项至关重要。

   pip3 install virtualenv

2. 安装 virtualenv 后，通过在终端中运行以下命令为我们的项目创建一个 Python 虚拟环境。

   virtualenv certora-env

3. 接下来，通过在终端中运行以下命令激活你创建的 Python 虚拟环境。

   source certora-env/bin/activate

4. 接下来，在终端中运行以下命令安装 Prover。

   pip3 install certora-cli

5. 接下来，使用以下命令在你的虚拟环境中安装 solc-select。这将使我们能够方便地更改我们正在使用的 Solidity 编译器版本。

   pip3 install solc-select

添加 Certora 个人访问密钥

要运行 Prover，你需要设置一个访问密钥作为系统变量。要获取你的个人访问密钥，请在 Certora 网站注册。注册后，你将收到 Certora 发送的一封电子邮件，其中包含访问密钥和 Certora 账户的初始密码。

要将访问密钥添加为系统变量，请遵循以下说明：

对于 Linux 用户

1. 打开终端并确保你位于项目目录中。

2. 使用 nano .profile 命令创建并打开 .profile 文件。

3. 要将访问密钥添加为环境变量，请在其中添加以下文本。

   #certora access key
   export CERTORAKEY=<your-certora-access-key>

4. 要保存更改，请按 CTRL + O，然后按 Enter。

5. 要退出，请按 CTRL + X。

6. 要在终端中加载我们对 .profile 文件所做的最新更改，请运行以下命令。

   source .profile

对于使用 zsh 的 Mac 用户

1. 打开终端并确保你位于 certora-counter 目录中。

2. 通过在终端中运行 nano .zshenv 命令创建一个名为 .zshenv 的文件。

3. 在你喜欢的文本编辑器中打开 .zshenv 文件。

4. 要将访问密钥添加为环境变量，请在其中添加以下文本。

   #certora access key
   export CERTORAKEY=<your-certora-access-key>

5. 要保存更改，请按 CTRL + O，然后按 Enter。

6. 要退出，请按 CTRL + X。

7. 要应用我们刚刚创建的环境变量，请在终端中运行以下命令。

   source .zshenv

请注意，每当你打开新的终端时，请务必运行 source .zshenv 或 source .profile 命令来加载环境变量；否则，你将收到 Prover 发出的错误消息 The environment variable CERTORAKEY does not contain a Certora key。

在项目目录中添加合约

在 certora-counter 目录中，添加一个名为 contracts 的子文件夹。完成后，在其中创建一个名为 Counter.sol 的文件，并添加以下合约。

//SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Counter {

    uint256 public count;

    function increment() external {
        count++;
    }
}

上面的合约是一个简单的智能合约，它只有一个名为 count 的公共状态变量，其值可以通过外部函数 increment() 递增。

设置 Certora Verification Language LSP

如果你使用 Microsoft 的 VS Code 编辑器或其分支版本，我们建议安装 Certora Verification Language LSP 以通过以下说明增强你的开发体验，包括语法检查、语法高亮和代码补全：

1. 在你的机器上打开 VS Code。
2. 通过单击侧边栏中的扩展图标打开扩展市场。
3. 在扩展搜索栏中搜索“Certora Verification Language LSP”。
4. 单击 Certora 发布的扩展上的“安装”。
5. 重新启动 VS Code 以完全激活扩展并应用所有更改。

编写你的第一个规范

在 certora-counter 目录中，添加一个名为 specs 的子文件夹。完成后，在其中创建一个名为 counter.spec 的文件，并添加以下代码。

methods {
    function count() external returns(uint256) envfree;
    function increment() external envfree;
}

rule checkCounter() {

    // Pre-Call State
    uint256 precallCount = count();

    // Method Call
    increment();

    // Post-call state
    uint256 postcallCount = count();

    // Assert that the post-call count is exactly one more than the pre-call count
    assert postcallCount == precallCount + 1;

}

目前，不必担心代码。我们将在下一章中详细剖析并解释每个部分。

添加 Solidity 编译器

在运行 Prover 之前，我们需要添加正确的 Solidity 编译器。要为我们的项目添加和使用正确的 Solidity 编译器版本，请在终端中运行以下两个命令。

solc-select install 0.8.25
solc-select use 0.8.25

运行验证

一旦我们有了合约和规范，我们就可以将它们提交给 Certora Prover 进行验证过程，方法是运行 certoraRun 命令。此命令需要 Solidity 合约的路径和相关的 .spec 文件，如下所示，才能成功执行。

certoraRun contractFilePath:contractName --verify contractName:specFilePath

要验证我们的规范，请确保你位于 certora-counter 目录中，然后在终端中运行以下命令。

certoraRun contracts/Counter.sol:Counter --verify Counter:specs/counter.spec

运行上述命令后，你应该会看到如下所示的输出。

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

然而，对于大型项目，直接在终端中使用带有许多参数的 certoraRun 命令可能会变得很麻烦。因此，建议使用配置文件。

使用配置文件简化 certoraRun 命令

在 Certora 中，配置文件是一个简单的 JSON5 文件，使用 .conf 扩展名编写，它至少需要两个关键参数以及其他配置选项：

• files：合约的路径以及合约名称。
• verify：规范文件的路径。

要使用配置文件，请在项目目录中创建一个名为 confs 的子文件夹。然后，在 confs 文件夹中创建一个名为 counter.conf 的文件，并添加以下内容。

{
    "files": [
        "contracts/Counter.sol:Counter"
    ],
    "verify": "Counter:specs/counter.spec",
}

将配置文件正确放置后，我们只需运行 certoraRun 命令并引用配置文件的路径即可执行验证过程，如下所示：

certoraRun confs/counter.conf

如果命令成功执行，你应该会看到如下所示的输出，其中包含一个验证结果的链接。

打开终端中打印的验证链接，查看验证结果。结果应与下图类似。

目前，只需了解绿色勾号 (✅) 表示 Prover 已成功验证规范文件 (counter.spec) 中指定的条件。这意味着合约已按照规范中概述的断言和逻辑按预期运行。

结论

恭喜！ 你已成功设置开发环境并执行了你的第一次形式化验证运行。然而，到目前为止，我们一直将规范文件 (.spec) 视为一个“黑匣子”。我们运行了它，但没有查看内部。在下一章中，我们将打开这个盒子并剖析 Certora 规范的结构。我们将分解其两个基本组成部分，即规则块（Rule Blocks）和方法块（Methods Blocks），并学习如何定义验证你的第一个智能合约所需的先决条件（pre-conditions）、动作（actions）和后置条件（post-conditions）。

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

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