Formal verification coverage

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

Evidence summary #

Certora conducted genuine formal verification: certora/ directory with CVL specs and certora_verification.yml CI in m0-foundation/protocol; separate Certora/M0-Protocol fork with formal specs. Prototech Labs delivered invariant test suite Jan-Feb 2024. Covers critical protocol invariants (earner rate indexing, collateral accounting, minting constraints). Exceptionally strong FV posture.

Sources #

GitHub
Certora M0-Protocol Formal Verification ForkCertora/M0-Protocol fork with CVL specsretrieved 2026-05-16
Audit
Prototech Labs Audit ReportPrototech Labs Audit Report — invariant test suiteretrieved 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 →

rubric_version v1.7.0 protocol m0 factor RD-F-009 score green collected_at 2026-05-16 09:46:19