Formal verification coverage
Uniswap (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 #
V3: ToB applied Manticore to BitMath and LiquidityMath properties — all verified. Certora independent FV research archived. V2: dapp.org.uk performed formal verification of v2-core. No comprehensive invariant list with full FV coverage for either version. Math primitives verified; economic invariants not fully covered. Combined: yellow.
Detail #
Trail of Bits README in v3-core audits directory documents Manticore verification results for 3 mathematical properties (BitMath.mostSignificantBit, BitMath.leastSignificantBit, LiquidityMathAddDelta — all Verified). Certora's AMM-UniswapV3-core repo (archived Oct 2022) demonstrates independent FV research on V3 core. For V2, the dapp.org.uk report includes formal verification of the core pair logic. However, neither version has published a comprehensive invariant specification with FV coverage metrics (e.g., what percentage of declared invariants are formally proven vs. tested). This falls into the partial-FV (20-79% coverage) yellow category.
Sources #
- GitHubCertora formal verification research on V3 core (independent)Certora/AMM-UniswapV3-core (archived)retrieved 2026-04-29
- dapp.org.uk — V2 formal verification + security reviewdapp.org.uk V2 audit (formal verification)retrieved 2026-05-12
- Trail of Bits — Manticore symbolic execution verification resultsv3-core/audits/tob/README.md — Manticore verification resultsretrieved 2026-05-12
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 →