The technical content top engineers rely on to level up.
9 min read
原生 Solana：程序入口与执行 在本系列的整个过程中，我们一直使用 Anchor 框架来构建 Solana 程序。本教程将教您如何使用原生 Rust 编写它们，而无需...
12 min read
Switchboard 链上程序无法直接访问链下数据。它们需要依赖预言机来引入资产价格、事件结果或 API 响应等信息。如果没有这些预言机，...
17 min read
Preserved Block 及其在不变量验证中的作用 不变量是一种在智能合约部署之后及其整个执行过程中必须始终保持成立的属性。乍一看，...
9 min read
ERC-721 中的 SafeMint 和 SafeTransfer 规则简介 本章是我们对 OpenZeppelin 的 ERC-721 CVL 规范代码解析的第四部分（4/5），重点关注形式化验证……
13 min read
在规则和不变量中使用 “requireInvariant” 到目前为止，我们要么编写一条规则来验证特定的行为，要么编写一个不变量来验证在整个……过程中必须始终成立的属性。
10 min read
使用 Ghost 和 Hook 验证不变量 在任何正确的 ERC20 实现中，所有账户余额的总和必须始终等于代币总供应量。这一属性应该始终保持成立......
12 min read
ERC-721 的部分参数化规则简介 本章是 OpenZeppelin 的 ERC-721 CVL 规范代码解析的最后一部分（5/5），该规范形式化验证了以下内容……
10 min read
在不变量中约束幽灵变量 在上一章中，我们看到了未受约束的幽灵变量会如何导致误报。我们还学习了如何使用语句来有效地约束……
17 min read
CVL 中的循环：路径爆炸与循环展开 循环是最常见的编程结构之一，但在形式化验证中，对它们进行推理仍然具有挑战性。虽然 Solidity 中的循环...
14 min read
ERC-721 的不变量介绍 在之前的章节中，我们探讨了 CVL 不变量的工作原理：在整个合约执行过程中必须始终成立的属性。不变量可以作为前置条件用于……
12 min read
Certora 中的不变量简介 到目前为止，我们一直专注于验证单个方法或方法序列的行为——确保特定的函数调用或一组调用......
10 min read
ERC-721 的铸造与销毁规则 简介 ERC-721 是以太坊的非同质化代币标准，被广泛用于表示数字财产。就像任何形式的财产一样，它围绕着供应展开……