The technical content top engineers rely on to level up.
9 min read
Persistent Ghosts 简介 在之前的章节中，我们使用了幽灵变量（通过 hooks）来记录在智能合约中未被显式追踪的存储值和数量——例如，...
14 min read
ERC-721 的不变量介绍 在之前的章节中，我们探讨了 CVL 不变量的工作原理：在整个合约执行过程中必须始终成立的属性。不变量可以作为前置条件用于……
8 min read
在规则中约束 Ghost 值 在上一章中，我们学习了 Ghost 变量如何让信息从 hook 流入规则。我们还了解到：在验证开始时……
12 min read
ERC-721 的部分参数化规则简介 本章是 OpenZeppelin 的 ERC-721 CVL 规范代码解析的最后一部分（5/5），该规范形式化验证了以下内容……
8 min read
ERC-721 的转移与授权规则介绍 本章是我们对 OpenZeppelin 的 ERC-721 CVL 规范代码解析的第三部分（3/5），重点关注代币转移……
17 min read
Preserved Block 及其在不变量验证中的作用 不变量是一种在智能合约部署之后及其整个执行过程中必须始终保持成立的属性。乍一看，...
13 min read
在规则和不变量中使用 “requireInvariant” 到目前为止，我们要么编写一条规则来验证特定的行为，要么编写一个不变量来验证在整个……过程中必须始终成立的属性。
10 min read
ERC-721 的铸造与销毁规则 简介 ERC-721 是以太坊的非同质化代币标准，被广泛用于表示数字财产。就像任何形式的财产一样，它围绕着供应展开……
5 min read
在 CVL 中测试 msg.sender 和 msg.value 简介 在本章中，我们将介绍 CVL 中的变量，这使我们能够为依赖于 、 以及……中的其他全局变量的函数制定规则。
8 min read
方法属性简介 简介 在上一章中，我们学习了参数化规则，这些规则使我们能够形式化验证预期成立的属性，无论哪个……
10 min read
形式化验证简介 形式化验证是通过数学方法证明程序符合规范的过程。本文将从概念上介绍形式化验证是如何……
7 min read
理解 Certora CVL 中的 Spec File 在上一章中，我们了解到，要使用 Certora Prover 进行形式化验证，我们需要向 Prover 提供以下关键项：智能...