The technical content top engineers rely on to level up.
5 min read
溢出与 Mathint 在 CVL 中，该类型表示无界整数，这与 Solidity 的固定大小类型（例如 .）不同。它在执行算术运算时不会发生溢出或下溢，从而允许基于...进行推理
5 min read
在 CVL 中测试 msg.sender 和 msg.value 简介 在本章中，我们将介绍 CVL 中的变量，这使我们能够为依赖于 、 以及……中的其他全局变量的函数制定规则。
10 min read
形式化验证简介 形式化验证是通过数学方法证明程序符合规范的过程。本文将从概念上介绍形式化验证是如何……
7 min read
在 Certora 中测试 Revert 调用 在本章中，我们将学习如何使用方法标签（和）以及 CVL 中的特殊变量，来验证智能合约执行中预期的 revert。准备工作...
5 min read
双条件运算符介绍 双条件运算符使我们能够在布尔值之间断言当且仅当（if-and-only-if）关系。蕴含（Implication）() 表明，如果条件 P 得到满足，那么 Q...
6 min read
形式化验证 Counter 在上一章中，我们学习了形式化验证的理论知识，包括它的概念以及它是如何工作的。在本模块中，我们将超越理论，进一步学习...
13 min read
Certora Require、Assert 和 Satisfy 在上一章中，我们了解到规范是一段用 CVL 编写的代码，用于描述智能合约的预期行为。一个……
6 min read
形式化验证 Ownable.sol Ownable 是一个提供基于所有者访问控制的抽象合约。当被继承时，它使用修饰符将特定函数限制为仅供所有者调用。它包含三个……
7 min read
理解 Certora CVL 中的 Spec File 在上一章中，我们了解到，要使用 Certora Prover 进行形式化验证，我们需要向 Prover 提供以下关键项：智能...
6 min read
形式化验证地址余额 在上一章中，我们介绍了如何在 CVL 中对环境依赖型函数进行推理，重点关注了非 payable 上下文。在这些示例中，访问......
4 min read
在 OpenZeppelin 中形式化验证 Nonces.Sol。Nonces 代表“number used once”（只使用一次的数字），被用于数字签名方案中以防止重放攻击。出于本文的目的，我们假设……
4 min read
形式化验证 Initializable.sol 本文介绍了 Certora 如何对 OpenZeppelin 的 Initializable.sol 合约进行形式化验证。我们假设读者已经熟悉该合约如何……