Formal verification coverage
Superstate'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 #
No evidence of Certora Prover, Halmos, Kani, or any formal verification tool applied to Superstate's EVM contracts. No .spec files or FV configuration found in the ustb GitHub repo tree. Docs reference only the 0xMacro audit series with no FV tooling mention. Per RWA regime (PD-042): formal verification of trust-mediated logic may be not_applicable for RWA issuers, but given the on-chain EVM surface ($1B TVS) formal verification would add meaningful assurance. Scored red on merits (0% critical invariant coverage).
Sources #
- GitHubsuperstateinc/ustb file tree (no FV files)GitHub API tree for superstateinc/ustb showing no .spec files, no FV configuration, no Certora/Halmos directoriesretrieved 2026-05-16
- Superstate documentation (no FV disclosure)Superstate docs: no mention of Certora, Halmos, Kani, or formal verificationretrieved 2026-05-16
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 →