Formal verification coverage
Spark Protocol'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 #
No formal verification (Certora, K-framework, or equivalent) applied to core SparkLend or sUSDS contracts. Audits substitute but do not provide the same mathematical guarantees for critical invariants.
Sources #
- Docshttps://docs.spark.fi/dev/security/security-and-auditsretrieved 2026-04-21
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 spark factor RD-F-009 score yellow collected_at 2026-04-27 01:00:42