Formal verification coverage

Lido'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 FV: Lido V2 (2023-04), Dual Governance (2025-02 + re-audit), V3 stVaults (2026-01-10), V3 Oracle (2026-01-10). Runtime Verification Dual Governance FV (2025-02). Verified invariants include escrow solvency, proportional share withdrawal, UnstETH locker exact-value withdrawal. Partial but high-quality FV coverage on critical paths.

Sources #

URL
SecurityReportshttps://github.com/Certora/SecurityReportsretrieved 2026-04-28
URL
lido-v2https://www.certora.com/reports/lido-v2retrieved 2026-04-28

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 →

rubric_version v1.7.0 protocol lido factor RD-F-009 score green collected_at 2026-04-28 13:58:42