Formal verification coverage

JustLend DAO'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 #

CertiK Skynet explicitly states 'No Properties Verified' for JustLend. No Certora, Halmos, or Kani FV specifications found in GitHub repository. CertiK audit used static analysis and manual review only. Zero formal verification coverage.

Sources #

Audit
CertiK Skynet JustLend — No Properties VerifiedCertiK Skynet: 'No Properties Verified' — confirmed absence of formal verificationretrieved 2026-05-17
GitHub
justlend-protocol GitHub repositoryGitHub repository — no FV spec files, no Certora/Halmos config foundretrieved 2026-05-17

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 justlend factor RD-F-009 score red collected_at 2026-05-17 10:25:32