Formal verification coverage
BlackRock USD Institutional Digital Liquidity Fund (BUIDL)'s assessment for RD-F-009 — scored not_applicable on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.
Evidence summary #
[PD-042 rescore 2026-05-12, v1.7.0+] Formal verification proves trustless invariants; this protocol's token logic is trust-mediated by the regulated issuer, so the FV factor is structurally malformed for this protocol type. Scored not_applicable per PD-042 (Cat 1 RWA-issuer subset). ORIGINAL EVIDENCE (preserved from v1.6.0 grading): No formal verification (Certora, Kani, Halmos) found for BUIDL contracts or Securitize platform. No FV report or specification files found in any public repository. Securitize GitHub shows no FV files.
Sources #
- GitHubhttps://github.com/securitize-ioretrieved 2026-04-26
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 →