Formal verification coverage
Aerodrome Finance'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 #
Trail of Bits verified three Uniswap v3 core mathematical invariants (BitMath.mostSignificantBit, BitMath.leastSignificantBit, LiquidityMath.addDelta) using Echidna property tests and Manticore symbolic execution for Slipstream. No Certora Prover specifications found. No formal declaration of protocol-wide Aerodrome-specific critical invariants found. Coverage estimated <20% of declared critical invariants formally verified.
Sources #
- GitHubTrail of Bits Slipstream audit README (Echidna/Manticore)ToB Slipstream README — Echidna and Manticore verification of 3 mathematical invariantsretrieved 2026-05-04
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 →