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.

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

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.

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.

We formally verified memory safety for inflate_table, a 266-line function in zlib where low-level memory operations depend on subtle algorithmic invariants. Starting without an existing C-to-Lean verification pipeline, we built one and produced a ~20,000-line Lean proof of memory safety and termination. LLMs generated most of the proof, while Lean checked every step.

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.