Certora Prover v8.1.0 版本发布，引入了多项重大变更，包括最低 Java 和 Python 版本要求提升、默认启用健全性检查、requireInvariant 语义更新、Solana 和 Soroban 验证需使用专用命令、默认报告链接改为私有、CVL 函数支持 revert 处理等。

本文讨论了Web3应用安全问题，特别关注智能合约的形式化验证。Certora通过形式化验证技术确保智能合约安全，并总结了五个Rust智能合约开发最佳实践，包括保持代码模块化、利用编译器检查、简化数据结构、减少trap value状态以及分离核心逻辑与副作用，以提高代码的可验证性和安全性。

infiniFi 是一个 DeFi 平台，旨在优化收益，但其 iUSD 赎回机制存在漏洞，可能导致用户在赎回队列中被跳过，从而面临不公平的惩罚。Certora Prover 发现了这一问题，并通过形式化验证确保了修复后的系统符合 FIFO 原则，维护了用户信任和 DeFi 协议的公平性。

本文介绍了Certora团队开发的一款用于验证编译器优化的等价性检查工具，该工具通过比较优化前后程序的行为来检测编译器bug。文章还分享了该工具在Vyper编译器中发现的一个优化bug，该bug导致局部变量被错误地映射到相同的堆栈位置，从而改变了程序的行为。该bug已在Vyper 0.4.2版本中修复。

infiniFi 是一个 DeFi 平台，通过管理 Pendle、AAVE 和 Ethena 等协议上的存款来优化收益。

Silo Finance 的一个新杠杆合约模块在测试阶段遭到攻击，由于过于宽泛的批准设置导致借款操控漏洞。该模块与核心Silo协议隔离，因此核心协议、金库、市场或用户资金未受影响。Certora 此前对该合约进行了安全审查，但未发现此漏洞，事后进行了风险评估和补救措施，并确认现有Silo代码是安全的。

本文介绍了Certora如何利用形式化验证来保护Uniswap v4免受恶意hook的攻击。通过Certora Prover工具，可以精确定义和证明正确性规则，从而确保智能合约的强大安全性。文章还展示了如何使用CVL编写规则，并利用Certora Prover进行验证，以检测通用hook的不当行为，从而保证资金处理的正确性。

本文强调了形式化验证（FV）在Web3和DeFi安全中的重要性，指出传统测试方法不足以应对Web3的安全挑战。FV通过数学证明确保代码按预期运行，能预防高危漏洞，并已在多个知名DeFi项目中应用，同时建议将FV尽早集成到开发生命周期中，以提升代码质量和安全性。

DeFi领域中的rounding errors漏洞依然普遍存在，可能导致重大损失。文章解释了rounding errors的成因、危害以及难以被人类发现的原因，并通过Juice Finance的案例展示了如何利用Formal Verification技术来检测和预防此类漏洞，强调了Formal Verification在保障DeFi协议安全中的作用。

Kamino Lending (KLend) is a lending protocol on Solana that emphasizes security through a partnership with Certora for rigorous code audits and formal verification。