Formal verification coverage
OpenEden's assessment for RD-F-009 — scored red on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.
Evidence summary #
No formal verification (Certora, Kani, Halmos, or equivalent) found in any public audit or repository. Neither Hacken nor Halborn engagements included FV scope. No FV spec files in the openeden.vault.audit GitHub repo. 0% coverage of declared critical invariants. This factor is scored rather than marked not_applicable because FV is applicable to any on-chain smart contract regardless of issuer type.
Sources #
- GitHubOpenEden Vault Audit Repo — GitHubopeneden.vault.audit repo — no FV spec files or Certora/Kani configurations presentretrieved 2026-05-16
- Hacken Security Audit — OpenEden Vault Nov-2024Hacken Nov-2024 — no FV scope mentionedretrieved 2026-05-16
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 →