Formal verification coverage

Jito'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 formal verification on Restaking+Vault (Oct 2024 + Dec 2024) and TipRouter NCN (Jan 2025). Covers restaking invariants (zero-supply VRT ratio, token validation, PDA verification). No FV coverage for StakeNet Steward or SPL Stake Pool. Partial coverage = yellow.

Sources #

Audit
Certora Jito Restaking V2 Formal VerificationCertora Restaking V2 FV report: covers zero-supply VRT ratio, unstaking logic, PDA verificationretrieved 2026-04-29
GitHub
Certora TipRouter Formal Verificationjito-tip-router security_audits/certora.pdf at ac76352retrieved 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 jito factor RD-F-009 score yellow collected_at 2026-04-29 15:50:23