Formal verification coverage
EigenLayer'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 has conducted at least 10 distinct formal verification engagements across EigenLayer (M4/PEPE Aug 2024; Duration Vaults Aug 2024; Incentive Council Aug 2024; V1.0.0 Slashing Feb 2025; MOOCOW Jun 2025; Multichain PT1 Jul 2025; Multichain pt2 Jul 2025; Merkle Jul 2025; Hourglass pt1 Aug 2025; Hourglass pt2 Aug 2025). A pre-launch Certora engagement detected a critical validator hazard in EigenPod checkpoint/Electra interaction and it was fixed before deployment. This represents among the strongest FV coverage in DeFi.
Sources #
- GitHubEigenLayer audits directory — Certora reportsLayr-Labs/eigenlayer-contracts/tree/main/audits — Certora engagements listingretrieved 2026-04-28
- Certora Electra Upgrade Critical FindingCertora — How EigenLayer Prevented a Critical Validator Hazard in Ethereum Electraretrieved 2026-04-28
- Certora EigenLayer Slashing Formal VerificationCertora EigenLayer Slashing Security Assessment and Formal Verification Reportretrieved 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 →