Formal verification coverage

Jupiter'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) identified for Jupiter programs. Audit index lists only traditional code review engagements — no FV reports. Solana/Rust/BPF FV tooling is less mature than EVM but not absent (Kani supports Rust). Protocol has not declared critical invariants subject to FV. No FV evident in any public source.

Sources #

Docs
Jupiter Audit Reports — Jupiter DevelopersAudit index — all engagements are traditional audits, no FV reports listedretrieved 2026-04-29

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 jupiter factor RD-F-009 score red collected_at 2026-04-29 11:51:25