Formal verification coverage
dYdX v4 (dYdX Chain)'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 #
Informal Systems actively uses Quint, Apalache, and TLA+-based model-based testing infrastructure. Per search evidence, they leverage these tools for Cosmos appchain audits. Whether specific v4-chain engagements included TLA+/Quint formal verification passes cannot be confirmed from public PDF contents (PDFs not parseable via WebFetch). Conservative yellow: firm capability confirmed, scope per engagement unverified.
Sources #
- URLdYdX Chain Audit — Informal Systems engagement scopedYdX chain audit blog — Informal Systems FV referenceretrieved 2026-05-17
- Quint — Informal Systems formal verification specification languageInformal Systems Quint FV toolingretrieved 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 →