在上一章中，我们学习了形式化验证的理论知识，包括它是什么以及它是如何工作的。在本模块中，我们将超越理论，学习以下内容：
- 如何配置与 Certora Prover 配合使用的项目。
- 如何获取并使用 Certora 访问密钥（access key）。
- 如何使用 Certora Prover 进行形式化验证。
让我们从为 Certora Prover 设置项目环境开始。
安装基本前提工具
在设置项目目录之前，请确保您的本地计算机已安装以下先决条件：
您只需在终端中运行 python3 --version 和 java --version 命令，即可检查您的计算机是否已安装这两者。
💡 对于 Windows 用户，我们强烈建议使用 Windows Subsystem for Linux (WSL) 以获得更好的体验。
设置我们的项目目录
安装好先决条件后，创建一个名为 certora-counter 的空目录，进入该目录，并按照以下说明正确设置您的项目目录。
- 在您的本地计算机上，通过运行以下命令安装 virtualenv。该工具将允许我们创建一个 Python 虚拟环境，这对于管理项目目录中的依赖项至关重要。
pip3 install virtualenv
- 安装好 virtualenv 后，通过在终端中运行以下命令为我们的项目创建一个 Python 虚拟环境。
virtualenv certora-env
- 接下来，通过在终端中运行以下命令激活您创建的 Python 虚拟环境。
source certora-env/bin/activate
- 接下来，在您的终端中运行以下命令以安装 Prover。
pip3 install certora-cli
- 接下来，使用以下命令在您的虚拟环境中安装 solc-select。这将使我们能够方便地更改所使用的 Solidity 编译器版本。
pip3 install solc-select
添加 Certora 个人访问密钥
要运行 Prover，您需要将访问密钥设置为系统变量。要获取您的个人访问权限，请在 Certora website 上注册。注册后，您将收到一封来自 Certora 的电子邮件，其中包含访问密钥和您 Certora 账户的初始密码。
要将访问密钥添加为系统变量，请遵循以下说明：
适用于 Linux 用户
- 打开终端并确保您在项目目录中。
- 使用
nano .profile命令创建并打开 .profile 文件。 - 要将访问密钥添加为环境变量，请在其中添加以下文本。
#certora access key
export CERTORAKEY=<your-certora-access-key>
- 要保存更改，请按
CTRL + O然后按Enter。 - 要退出，请按
CTRL + X。 - 要加载我们最近在 .profile 文件中所做的更改，请在您的终端中运行以下命令。
source .profile
适用于使用 zsh 的 Mac 用户
- 打开终端并确保您在
certora-counter目录中。 - 通过在终端中运行
nano .zshenv命令，创建一个名为 .zshenv 的文件。 - 在您喜欢的文本编辑器中打开
.zshenv文件。 - 要将访问密钥添加为环境变量，请在其中添加以下文本。
#certora access key
export CERTORAKEY=<your-certora-access-key>
- 要保存更改，请按
CTRL + O然后按Enter。 - 要退出，请按
CTRL + X。 - 要应用我们刚刚创建的环境变量，请在终端中运行以下命令。
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，通过语法检查、语法高亮和代码补全来提升您的开发体验：
- 在您的计算机上 打开 VS Code。
- 点击侧边栏中的扩展图标 打开扩展市场 (Extensions Marketplace)。
- 在扩展搜索栏中 搜索“Certora Verification Language LSP”。
- 找到由 Certora 发布的扩展，点击“Install（安装）”。
- 重启 VS Code 以完全激活该扩展并应用所有更改。
编写您的第一个规范 (Specification)
在 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
运行验证
一旦我们有了合约和规范，就可以通过运行 certoraRun 命令将它们提交给 Certora Prover 进行验证过程。该命令需要 Solidity 合约的路径以及相关的 .spec 文件才能成功执行，如下所示。
certoraRun contractFilePath:contractName --verify contractName:specFilePath
要验证我们的规范，请确保您在 certora-counter 目录中，然后在终端中运行以下命令。
certoraRun contracts/Counter.sol:Counter --verify Counter:specs/counter.spec
运行上述命令后，您应该会看到类似如下的输出。
要查看验证结果，请打开终端中打印的验证链接。结果应类似于下图。
然而，对于大型项目，直接在终端中使用带有许多参数的 certoraRun 命令可能会变得繁琐。因此，建议使用配置文件。
使用配置文件简化 certoraRun 命令
在 Certora 中，配置文件是一个使用 .conf 扩展名编写的简单 JSON5 文件，它至少需要两个关键参数以及 其他配置选项：
- 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）视为一个“黑盒（black box）”。我们运行了它，但没有去查看里面的内容。在下一章中，我们将打开这个黑盒并剖析 Certora 规范的结构。我们将分解其两个基本组成部分：规则块（Rule Blocks）和方法块（Methods Blocks），并学习如何定义验证您的第一个智能合约所需的前置条件、操作和后置条件。
本文是关于 使用 Certora Prover 进行形式化验证 系列文章的一部分