不变式

本文深入探讨了Wrapped ETH（WETH）智能合约的安全性和完整性验证。重点说明了通过使用Z3 SMT求解器所证明的两个重要不变式：WETH的内部会计正确性以及其用户始终能够成功提取已存款的ETH。此外，文章还提及了在WETH合约实现中发现的一个无害的小错误，并讨论了进一步的研究方向。

本文详细介绍了如何使用Certora Prover对Solmate的ERC-20代币进行形式化验证。内容涵盖了如何验证`transfer`、`transferFrom`、`approve`、`mint`和`burn`等函数的正确性（包括成功和回滚场景），确保没有意外的副作用，以及定义和验证如“总余额等于总供应量”等关键不变式。文章还探讨了如何防止未经授权的操作，并提供了具体的CVL规则示例。

本文详细介绍了如何使用 Certora Prover 对 Solady WETH 智能合约进行形式化验证。文章通过具体的 CVL 规则和不变式，深入分析了 WETH 的存取款功能及其核心不变性，包括处理以太坊余额、WETH 总供应量变化、事务回滚条件以及利用 `ghost` 变量和 `hook` 处理底层调用，最终展示了如何用 `requireInvariant` 优化验证。

本文详细阐述了如何使用Certora Prover对ERC-721代币合约进行形式化验证，重点介绍了5个关键不变式（invariants）的实现与验证。

这篇文章详细介绍了使用 Certora 工具进行形式化验证中的参数化规则（Parametric Rules）。它解释了如何通过定义通用规则来验证智能合约在任何函数调用后都应保持不变的属性，例如 ERC-20 代币的总供应量不变性，并深入探讨了参数化规则的作用范围和执行机制。

本文详细介绍了 Certora 形式化验证工具中 `requireInvariant` 语句的用法。它通过在规则和不变式中引入已证明的不变式作为假设，避免了在不切实际的合约状态下进行验证，从而提高了验证的效率和准确性。文章以 ERC20 代币的 `transfer` 函数为例进行了实践演示。

本文是一份智能合约审计范围界定指南，详细介绍了审计准备阶段需要向审计公司提供的七项关键资料：冻结的代码提交哈希、可重现构建、测试套件、三层文档、角色权限表、不变式列表和已知可接受问题列表。文章解释了为何审计的报价和工期在审计师开始处理代码的第一小时内就已决定，而非签署合同时。通过完善的准备，团队可将审计成本降低15-30%。还提供了根据nSLOC（代码行数）估算成本和工期的参考表，以及Rekt测试的12个问题，帮助团队自查审计准备程度。最后给出完整的审计前资料包清单。

文章详细介绍了模糊测试及其在Solidity智能合约安全中的应用。它解释了模糊测试如何通过生成随机输入来发现传统测试遗漏的边缘案例，并深入阐述了不变式（Invariants）的概念及其在DeFi协议中确保系统稳定性的关键作用。文章还探讨了无状态与有状态模糊测试、边界模型检查以及模糊测试与端到端测试的结合。