Formal verification coverage
QuickSwap'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 core: ABDK Consulting produced formal specifications and proofs using act specification language and K framework for UniswapV2Pair and UniswapV2Factory — this constitutes formal verification of critical invariants (constant-product invariant, flash-swap accounting). QuickSwap V2 inherits this coverage by zero-divergence. V3/Algebra: no Certora/Kani/Halmos formal verification found. Hacken, Hexens, and ABDK audits are traditional security audits, not formal verification. Yellow: V2 has FV coverage; V3 Algebra (the majority of current TVL usage) does not.
Sources #
- AuditABDK Uniswap V2 Formal Verification ReportABDK V2 formal verification using act + K framework (Jan-Apr 2020)retrieved 2026-05-16
- Algebra Audits Completed BlogAlgebra audit blog — traditional security audits (not FV)retrieved 2026-05-16
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 →