不变量

这篇文章详细介绍了Curve StableSwap中的`get_D()`和`get_y()`函数的数学推导过程，分析了如何通过牛顿法计算流动性池的D值，以及如何在保持平衡的条件下调整代币的值。文章深入探讨了StableSwap的不变量公式，并与实际代码进行了对比，有助于读者理解流动性池的工作原理和算法优化。

本文深入探讨了 Certora 形式化验证中，如何在不变量（invariants）内正确约束幽灵变量（ghost variables）。文章指出 `require` 语句不适用于不变量，并详细介绍了使用 `init_state axiom` 来设置幽灵变量的初始值，以及使用 `global axiom` 来定义在所有状态下都成立的属性，以解决验证失败的问题。

文章详细介绍了使用 Certora 进行智能合约形式化验证中的核心概念：不变量（Invariants）。它解释了不变量与规则（Rules）的区别，深入探讨了如何使用 Certora Verification Language (CVL) 定义、设置和验证智能合约中的不变量，并阐述了Certora Prover基于数学归纳法的验证原理和优化机制。

这篇文章详细介绍了 Certora 形式化验证中“保留块”（preserved blocks）的作用和用法。它解释了如何利用保留块来指导 Certora Prover 避免在探索不切实际的符号状态时产生虚假告警，从而确保对智能合约不变量（invariants）的验证更加准确和有效。文章以 WETH 合约为案例，逐步演示了如何通过添加保留块来解决验证失败的问题。

本文深入探讨了在Certora形式化验证中使用Sstore Hook来处理智能合约中的存储映射（storage mappings）的挑战和解决方案。

本文详细介绍了如何使用Certora Prover对ERC-721代币的`transferFrom()`、`approve()`、`setApprovalForAll()`以及`balanceOf(0)`等核心功能进行形式化验证。文章通过具体的Certora验证语言（CVL）代码示例，深入解析了每个规则的前置条件、状态记录、方法调用以及活性、效果和无副作用断言，旨在确保代币操作的正确性和安全性。

作者使用AI代理Cygent为其Rust游戏仿真项目Alembic（8500行，零测试）生成测试。通过结构重构、识别不变量、与Claude Code协作，最终生成116个集成测试，覆盖9个子系统，并发现两个实际bug。工作流包括Kyle（Cygent）实现、Claude Code审查、人类决策。测试套件作为回归网持续运行，自动触发新测试生成和PR审查。

文章讲述了 Notional Finance 系统中出现的一个漏洞，该漏洞由于不正确的形式化验证不变量导致。原本旨在防止资产重复的错误不变量实际上是空洞的，无法发现漏洞。随后通过更正后的简单不变量成功检测到该漏洞，并提出了改进规范安全性的措施，包括审计规范、漏洞赏金、技术检查和集成测试工具，以提高代码安全性和规范的准确性。

本文探讨了形式化验证和模糊测试在智能合约安全审计中的应用。文章指出，形式化验证虽然理论上可以证明代码中不存在漏洞，但在实际复杂代码库中难以实现，并且模糊测试可以发现形式化验证所能发现的相同漏洞。文章建议在采用形式化验证之前，应优先使用模糊测试，并强调编写高质量不变量的重要性。

本文主要介绍了在将智能合约项目提交给安全审计之前，如何进行充分的准备工作。内容涵盖了项目准备的重要性，包括清晰地阐述协议概念、工作流程，提供合约概述，明确不变量，以及使用完善的库。此外，文章还强调了开发过程中的良好实践，如遵循Solidity的最佳实践、进行充分的测试和内部安全审查，并提供了关于安全性考虑和定义安全审查范围的建议。

本文讨论了2026年智能合约审计领域的变化，包括审计定价从按代码行数到按逻辑密度估值转变，AI在审计工作流程中的集成应用，以及获得顶级公司审计资格的技术先决条件。文章强调了智能合约安全动态对于项目生存的重要性，并为协议领导者提供了战略检查清单。

本文探讨了模糊测试在智能合约安全中的重要性，包括无状态模糊测试和有状态模糊测试的基本概念及应用。通过验证不变量，开发者能有效识别潜在漏洞，从而提升智能合约的安全性。文章强调模糊测试并非替代手动审查的灵丹妙药，而是与其他安全措施相结合的必要步骤。

本文分析了 Damn Vulnerable DeFi V4 的 Unstoppable 挑战，该挑战通过操纵会计系统实现拒绝服务攻击。

Certora 对 Sui 链上的借贷协议 Suilend 进行了形式化验证，重点分析了系统级不变量。验证涵盖了偿付能力、账户健康度以及清算盈利性三个维度，识别并修复了包括双重舍入漏洞、算术舍入漂移以及特定 LTV 条件下清算导致资产状况恶化等技术问题，确保了协议的整体安全性。

这篇文章主要介绍了 Certora Prover 的新更新，包括 CVL 中新增的 links 块，用于更直观、类型安全地把合约存储变量绑定到目标合约；TAC dump 的可视化诊断能力增强，支持前进后退、变量联动高亮和数据流图；以及 requireInvariant 在强不变量场景下的语义改进，降低外部调用后出现误报反例的概率。同时，文章还说明了 GitHub App 的评论配置新选项 gh-review 与 gh-review-jobs，并给出升级到 8.11.3 的方式。