Formal verification coverage

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

Evidence summary #

Runtime Verification conducted a formal verification engagement in May 2023 covering EVM contracts (listed in wormhole-audits as "EVM formal verification"). The scope of invariants covered and % coverage is not publicly documented in the accessible report listing. Certora is not mentioned in the Wormhole audit list. The Runtime Verification engagement exists but coverage metrics are not accessible without the PDF.

Sources #

Curator note
Extracted from 01-code-security.md — RD-F-009 finding; no URL cited in originalretrieved 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 wormhole factor RD-F-009 score yellow collected_at 2026-04-28 01:38:43