Starknet 上的 Library call：Library call 会在调用它的合约的上下文和存储中，执行已声明的 contract class 的逻辑。这与 Solidity 的机制类似，但使用的是 class hashes...

Starknet 上的哈希函数：Solidity 依赖 keccak-256 作为其主要哈希函数，用于从任意数据中推导出确定性标识符，例如计算函数选择器或计算存储......

Starknet 中的系统调用 在 Solidity 中，读取/写入存储、合约间调用或发送消息等底层操作，都是直接使用 Yul 通过内联汇编来执行的...

在规则和不变量中使用 “requireInvariant” 到目前为止，我们要么编写一条规则来验证特定的行为，要么编写一个不变量来验证在整个……过程中必须始终成立的属性。

ERC-721 的部分参数化规则简介 本章是 OpenZeppelin 的 ERC-721 CVL 规范代码解析的最后一部分（5/5），该规范形式化验证了以下内容……

Preserved Block 及其在不变量验证中的作用 不变量是一种在智能合约部署之后及其整个执行过程中必须始终保持成立的属性。乍一看，...

Certora 中的不变量简介 到目前为止，我们一直专注于验证单个方法或方法序列的行为——确保特定的函数调用或一组调用......

在不变量中约束幽灵变量 在上一章中，我们看到了未受约束的幽灵变量会如何导致误报。我们还学习了如何使用语句来有效地约束……

形式化验证 Solady WETH 简介 ETH 广泛用于 DeFi 中的兑换、流动性提供、质押和抵押，因此需要一个兼容 ERC-20 的版本，以便协议可以通过...与其进行交互

ERC-721 的不变量介绍 在之前的章节中，我们探讨了 CVL 不变量的工作原理：在整个合约执行过程中必须始终成立的属性。不变量可以作为前置条件用于……

CVL 中的循环：路径爆炸与循环展开 循环是最常见的编程结构之一，但在形式化验证中，对它们进行推理仍然具有挑战性。虽然 Solidity 中的循环...

在规则中约束 Ghost 值 在上一章中，我们学习了 Ghost 变量如何让信息从 hook 流入规则。我们还了解到：在验证开始时……