Formal verification coverage

Sky Lending (formerly MakerDAO)'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 #

Runtime Verification K-specification covers MCD core invariants (2019). Certora FV specs present in sky-ecosystem/usds (Usds.spec, DaiUsds.spec, UsdsJoin.spec). Newer modules (stUSDS, LockStake) do not have documented FV coverage. Partial FV across the system.

Sources #

URL
https://github.com/sky-ecosystem/usds/tree/master/certoraretrieved 2026-04-27
URL
https://security.makerdao.com/formal-verificationretrieved 2026-04-27
URL
https://github.com/makerdao/mkr-mcd-specretrieved 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 →

rubric_version v1.7.0 protocol sky-lending factor RD-F-009 score yellow collected_at 2026-04-28 00:43:18