本文介绍了Compound新协议Comet的一个有趣的正确性规则，以及在早期开发过程中如何利用Certora Prover进行形式化验证，以消除代码中的bug。通过形式化规范和验证，团队成功发现并修复了一个导致用户抵押资产状态错误的bug，从而提高了协议的安全性。

本文详细描述了在 Balancer V2 中发现的一个由 Certora 团队通过形式化验证发现的偿付能力漏洞。该漏洞允许用户通过将贷款分割成小额多次来逃避闪电贷费用，从而导致 Vault 的偿付能力受损。Balancer 团队通过要求 token 地址数组按严格升序排列解决了这个问题。

本文揭示了在Solidity编译器版本0.8.3及以下中存在的内存隔离漏洞，该漏洞影响了ABI反序列化过程，可能导致恶意字节缓冲区的攻击。作者详细解释了ABI规范、序列化和编码格式，以及引入的具体漏洞和影响，并指出该漏洞已在0.8.4版本中修复。

文章详细介绍了在Solidity编译器中发现的一种代码生成漏洞，允许恶意存储字段欺骗Solidity，将不相关信息插入通过abi.encodePacked等方法生成的数组中。该漏洞已在Solidity 0.8.0版本中修复。

Certora团队的John Toman发现了Solidity 0.7.3中的一个bug，该bug导致编译器在一些写入操作中错误地将垃圾数据写入持久存储。这一问题可能导致合同执行成本增加，但目前尚未确认其安全影响。Solidity编译器团队已在0.7.4版本中修复了该bug。

本文讨论了2019年在Solidity编译器中发现的一个内存管理漏洞，导致动态数组的长度计算溢出，并可能导致内存损坏。文章深入分析了该漏洞的原理、示例代码及其潜在影响，还探讨了如何避免及检测此类漏洞的方法。最后，作者提到应用形式化方法来提高编译器的正确性和区块链智能合约的安全性。