Formal verification coverage
ether.fi'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 active retainer: 15 FV reports from 2024-10 to 2026-03 covering eETH share inflation, withdrawal fee, v2.49 core, EigenLayer slashing integration, V3.Prelude, Pectra features, weETH adapter, safe key gen + consensus role, core contracts re-audit, and priority queue. EtherFiOracle.spec present in certora/specs directory. Core contracts (LiquidityPool, eETH, weETH) formally verified in 2026-01-29 re-audit. One of the strongest ongoing FV postures in the LRT sector.
Sources #
- GitHubCertora specs and config directoryetherfi-protocol/smart-contracts/tree/master/certoraretrieved 2026-04-28
- 15 Certora FV reports 2024-10 through 2026-03etherfi-protocol/smart-contracts/tree/master/audits (Certora reports)retrieved 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 →