形式化验证

本文介绍了如何形式化验证Plonky2中的U32AddManyGate。通过从Rust导出多项式约束到Lean，将约束通用化并编写基于自然数算术的规范，然后证明约束满足推导出规范（可靠性）以及规范存在时约束可满足（完备性）。验证过程发现了一个隐式假设：进位输入必须≤15，而接口允许更大值，这可能导致不完整。该工作为Lighter项目提供了可信任的电路基础。

本文介绍了如何在 Certora Verification Language (CVL) 中使用 if/else 语句和三元运算符进行形式化验证。通过实例展示了对 Solidity 合约中条件行为（如溢出处理、max 函数）的验证，并强调了优化 CVL 规则以提高验证效率的重要性。文章还讨论了 if/else 的局限性及三元运算符的适用场景。

文章详细介绍了如何使用Certora形式化验证工具中的`@withrevert`方法标签和`lastReverted`特殊变量来验证智能合约中的预期revert行为。它解释了Certora Prover默认忽略revert的原因，以及如何显式地处理revert路径，从而确保合约在所有情况下（包括溢出等异常情况）的行为符合预期。

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

本文深入探讨了如何使用Certora的存储Hook（Storage Hooks）和幽灵变量（Ghost Variables）进行智能合约的形式化验证。文章通过具体案例，详细阐述了如何观察合约内部私有状态的变化，并克服了规则无法直接访问Hook局部变量的限制，最终实现了对合约关键属性的精确验证。

本文揭示了有关智能合约形式验证（FV）的三大常见误解，并介绍了Certora开发的形式验证语言CVL如何有效打破这些误区。文章通过示例展示了CVL的易用性和强大能力，强调了形式验证在检查合约安全性和发现复杂漏洞中的重要性，以及Certora Prover工具的实际应用。

本文详细介绍了Silo融资协议中的一个关键漏洞及其修复过程。通过Certora的形式验证工具进行深入分析，报告总结了漏洞的产生原因、修复方法及验证过程，并提出了未来加强规则和安全性的计划。

本文详细介绍了形式化验证（formal verification）的过程及其在智能合约中的应用，强调了与单元测试的互补关系，以及如何利用Halmos工具简化形式化验证的实施。文中分析了正式验证的挑战、规范的编写开销及其在ERC721A智能合约中的案例，展示了通过符号测试实现高效验证的重要性。

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

这篇文章介绍了 V 规范语言，主要用于形式验证以证明程序逻辑的正确性。文章详细阐述了 V 语言的核心构建块—— V 语句，以及如何使用它们来指定智能合约的属性、合约不变性、方法合约和行为规范，强调了这些规范在开发安全智能合约中的重要性。

这篇文章深入探讨了在使用Certora进行形式化验证时，Solidity合约中`unchecked`块可能引发的问题。它解释了Prover如何在这种情况下错误地假设溢出行为，并通过引入`Sload`Hook来明确定义幽灵变量与存储变量之间的关系，从而修复验证中的假阳性问题。

本文深入探讨了使用Certora Prover对ERC-721代币中的_safeMint()和safeTransferFrom()功能进行形式化验证。文章详细解释了如何通过模拟合约和CVL（Certora验证语言）的辅助函数来处理外部回调，以确保验证的完整性，并阐述了活性、效果和无副作用断言。

本文详细介绍了 Certora 形式化验证中 CVL 语言的 `require`、`assert` 和 `satisfy` 语句。它解释了这些语句如何定义智能合约的预期行为、约束验证过程，并演示了它们在确保合约正确性及查找解决方案中的应用场景和区别。

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

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