Formal verification coverage
Kamino Lend'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 #
Certora Prover applied across 7 version-specific engagements (v1.13.0–v1.17.0) focusing on solvency invariants; OSEC also performed formal verification. Coverage % of all declared critical invariants not publicly quantified.
Detail #
Two separate FV engagements cover the core lending primitive. The exact percentage of declared critical invariants verified is not stated in the publicly accessible report summary. Scored yellow: FV clearly performed and meaningful (caught the precision loss bug), but coverage comprehensiveness cannot be confirmed without PDF parsing.
Sources #
- GitHubKamino Finance Audits RepositoryOSEC formal verification: kamino_lend_osec_formal_verification.pdfretrieved 2026-04-27
- Certora Securing Kamino LendingCertora blog — formal verification of Kamino Lending Protocol using Certora Proverretrieved 2026-04-27
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 →