Formal verification coverage
Liquid Collective (LsETH)'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 Nov 2024 used the Certora Prover (CVL specification language). The certora/specs directory contains 19 specification files covering AllowlistV1, ConsensusLayerDepositManagerV1, CoverageFundV1, Firewall, OperatorRegistryV1, RedeemManagerV1, RiverV1, SharesManagerV1, and UserDepositManagerV1. Certora confirmed 'Prover demonstrated implementation is correct with respect to formal rules.' This is genuine Prover-based FV with broad contract coverage. A dedicated RiverV1DivideOnlyByConstant.spec also shows mathematical invariant coverage.
Sources #
- URLLiquid Collective Completes Full Formal VerificationFormal verification completion blog postretrieved 2026-05-17
- Certora Report — Alluvial Finance / Liquid CollectiveCertora Prover engagement — mathematical correctness confirmationretrieved 2026-05-17
- Certora specs directory — liquid-collective-protocolcertora/specs directory listing 19 specification files for core contractsretrieved 2026-05-17
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 →