本文详细描述了在 Balancer V2 中发现的一个由 Certora 团队通过形式化验证发现的偿付能力漏洞。该漏洞允许用户通过将贷款分割成小额多次来逃避闪电贷费用，从而导致 Vault 的偿付能力受损。Balancer 团队通过要求 token 地址数组按严格升序排列解决了这个问题。
本文讨论了Certora如何对Euler V2 Vault的关键属性进行形式验证，从而提高DeFi协议的安全性。具体介绍了形式验证如何帮助发现开发者未发现的罕见漏洞，以及如何确保用户账户的健康性和协议的偿付能力。作者提供了详细的实例和实现细节，强调了良好的规范设计在形式验证中的重要性。
uri_kirstein
Certora