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

本文详细介绍了Certora形式化验证工具中双向条件运算符（<=>）的用法，并将其与蕴含运算符（=>）进行了比较。通过Solidity的setX()函数和Solmate的mulDivUp()函数为例，演示了如何使用双向条件运算符更简洁、明确地表达代码的逻辑关系和行为，特别是在验证函数成功条件、revert条件和舍入行为时的应用。

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

本文深入探讨了Certora形式化验证工具中CVL语言的mathint类型，该类型代表无界整数，能有效检测Solidity合约（尤其是在unchecked块和内联汇编中）可能发生的溢出或下溢问题。文章强调了mathint的默认行为及其在暴露潜在漏洞方面的优势，并警告了将mathint强制转换为uint256的危险性，因为这可能掩盖错误。

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

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

本文介绍了如何使用Certora工具通过幽灵变量（ghost variables）和Hook（hooks）对ERC20代币合约进行形式化验证，确保“总供应量等于所有账户余额之和”这一核心不变性。文章详细阐述了在Sstore和SloadHook中放置约束条件的不同影响，并强调了SloadHook在排除不可能状态方面的优越性。

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

这篇文章详细介绍了如何使用 Certora 形式化验证工具来验证 Solidity 合约中与支付（payable 函数）、交易金额（msg.value）和账户余额相关的属性。通过具体的合约示例和 CVL 规则，逐步展示了如何处理潜在的故障情况（如余额不足、自调用），并利用 Certora Prover 发现并修复反例，旨在确保智能合约的安全性。

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