Formal verification coverage
Marinade Finance'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 coverage. The GitHub repo, docs, and all five audit PDFs make no mention of Certora, Kani, Halmos, or any formal verification tool. The 2023 Neodyme and Sec3 engagements were traditional security audits, not FV. Kani (Rust model checker) could theoretically apply to this Solana/Rust codebase but has not been used. Zero percent of declared invariants are formally verified.
Sources #
- GitHubMarinade liquid-staking-program READMEGitHub README — no formal verification mentionedretrieved 2026-05-16
- Marinade Finance Security AuditsMarinade security and audits docs — no FV reportedretrieved 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 →