Formal verification coverage
Liquity V1 + V2 (LUSD / BOLD)'s assessment for RD-F-009 — scored green on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.
Evidence summary #
Certora formal verification for v2 (December 2024) covers batch delegation logic and interest rate management invariants — two of the most complex v2 subsystems. Certora report is publicly available. Additionally, Recon review documented extensive invariant specifications covering trove sorting, debt accounting consistency, batch PPFS monotonicity, and collateral surplus changes. This represents substantive FV coverage for an original protocol. v1 had no formal verification (Trail of Bits 2021 pre-dates widespread FV practice), but score is on the operative v2 version. Per profile §11 flag, this is a formal verification exemplar.
Sources #
- URLAuditing Liquity V2 (Liquity blog)Liquity v2 auditing blog confirming Certora FV engagementretrieved 2026-05-16
- Bold Protocol Security Review / Invariant Documentation (Recon)Recon review with extensive invariant documentation (trove sorting, debt accounting, batch PPFS, collateral surplus)retrieved 2026-05-16
- Certora Liquity Formal Verification Report (Dec 2024)Certora Liquity v2 formal verification report, December 2024, scope: batch delegation + interest rate managementretrieved 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 →