Browse all Solidity articles.
14 min read
形式化验证 ERC-20 代币简介 在本章中，我们将形式化验证 Solmate 的 ERC-20 实现，其中包括以下内容： 标准的状态修改函数： , , 标准视图...
10 min read
在不变量中约束幽灵变量 在上一章中，我们看到了未受约束的幽灵变量会如何导致误报。我们还学习了如何使用语句来有效地约束……
8 min read
在规则中约束 Ghost 值 在上一章中，我们学习了 Ghost 变量如何让信息从 hook 流入规则。我们还了解到：在验证开始时……
7 min read
在 Storage Mappings 中使用 Sstore Hooks 简介 在“Storage Hooks 和 Ghosts 简介”一章中，我们介绍了简单存储变量的 storage hooks 和 ghosts。我们展示了...
12 min read
ERC-721 的部分参数化规则简介 本章是 OpenZeppelin 的 ERC-721 CVL 规范代码解析的最后一部分（5/5），该规范形式化验证了以下内容……
15 min read
Storage Hooks 与 Ghosts 简介 通常我们需要检查特定存储位置的更改，以证明某个属性或不变量成立，特别是当该存储不...
10 min read
使用 Ghost 和 Hook 验证不变量 在任何正确的 ERC20 实现中，所有账户余额的总和必须始终等于代币总供应量。这一属性应该始终保持成立......
10 min read
ERC-721 的铸造与销毁规则 简介 ERC-721 是以太坊的非同质化代币标准，被广泛用于表示数字财产。就像任何形式的财产一样，它围绕着供应展开……
5 min read
溢出与 Mathint 在 CVL 中，该类型表示无界整数，这与 Solidity 的固定大小类型（例如 .）不同。它在执行算术运算时不会发生溢出或下溢，从而允许基于...进行推理
8 min read
方法属性简介 简介 在上一章中，我们学习了参数化规则，这些规则使我们能够形式化验证预期成立的属性，无论哪个……
7 min read
理解 Certora CVL 中的 Spec File 在上一章中，我们了解到，要使用 Certora Prover 进行形式化验证，我们需要向 Prover 提供以下关键项：智能...
10 min read
蕴含运算符简介 蕴含运算符常被用作该语句的替代方案，因为它更加简洁。考虑以下示例：一个接受两个无符号...