Formal verification coverage
Balancer (v2 + v3)'s assessment for RD-F-009 — scored yellow on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.
Evidence summary #
v2: Certora 2021-04 FV (Vault), Certora 2022-09 FV (ComposableStablePool). The 2022 FV proved high-level solvency invariants (sum of BPT <= totalSupply; no BPT minted without asset increase) but explicitly did not verify rounding behavior or swap reversibility — the missing properties that would have caught the Nov 2025 exploit. v3: Certora 2024-09 FV (Vault, Weighted, Stable) plus Certora 2026-01 comprehensive assessment reportedly no critical findings. v3 FV incorporates lessons from v2 exploit (post-Certora-blog: roundtrip swap invariance and BPT share value preservation would have caught the bug). FV coverage exists but v2 FV had critical gaps proven by the exploit.
Sources #
- URLCertora: Breaking Down the Balancer Hackhttps://www.certora.com/blog/breaking-down-the-balancer-hackretrieved 2026-05-05
- Balancer v3 audit reports directoryhttps://github.com/balancer/balancer-v3-monorepo/tree/main/auditsretrieved 2026-05-05
Methodology #
Determine the percentage of protocol-declared critical invariants covered by a formal verification proof (Certora Prover, Kani, Halmos, or equivalent).
See the full factor methodology and distribution across all protocols →