Certora recently raised the bar for DeFi security by formally verifying a key property of the Euler V2 Vault implementation. In this post we talk about how formal verification can offer strong assurance about DeFi protocols, find rare bugs unknown to developers, and even involve specifications that are simpler to understand than exploits.