Formal verification coverage

GMX v2 (GMX Synthetics)'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 #

Certora ran FV on six modules (Bank, DataStore, Oracle, OracleStore, RoleStore, StrictBank) Aug 7-28 2023, with 39 wardens and 28 mutation test cases. No explicit overall invariant coverage percentage stated. Coverage is partial - the 6 modules covered are the most critical primitives but the full 95-contract system was not formally verified.

Sources #

URL
Certora GMX Formal Verification ReportCertora GMX formal verification report - 6 modules, 28 mutation tests, no overall % statedretrieved 2026-05-05

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 gmx-v2 factor RD-F-009 score yellow collected_at 2026-05-05 11:15:06