Certora compared AutoProver’s independently generated Aave v4 Hub specification with a human-authored verification engagement. AutoProver discovered and proved substantial solvency and accounting properties, but the comparison also revealed why generated coverage must be paired with expert analysis of protocol intent and economic safety.

How to design Solidity smart contracts that are easier to formally verify.

On November 3, 2025, Balancer suffered an incident in which attackers manipulated internal vault logic to drain liquidity across multiple blockchains. The breach underscores the importance of prioritizing security even for mature protocols with multiple audits, and it raises urgent questions about composability, operational controls, and the evolving threat-landscape in Web3. Here is Certora’s analysis of the incident, as well as a detailed timeline of events.

Our engineers identified and corrected a subtle but significant issue in infiniFi's redemption logic through rigorous formal verification, ensuring fairness and trustworthiness. The team ensured that users are treated consistently and predictably under all conditions.

Kamino Lending partnered with Certora's formal verification to identify and resolve a subtle rounding issue in its Solana-based lending protocol, proactively securing it against potential future exploits.