defirisk.co
rubric v1.7.0

Formal verification coverage

Ethena's assessment for RD-F-009 — scored gray on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.

Evidence summary #

No formal verification (Certora, Halmos, Kani) has been published for Ethena contracts. Chaos Labs provided economic risk analysis only (not FV). No FV coverage found in any of the 13 audit engagements.

Sources #

  • Docs
    Audits | EthenaEthena audit list — no FV reports listedretrieved 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 ethena factor RD-F-009 score gray collected_at 2026-04-28 13:58:51