Formal verification coverage

Axelar Network's assessment for RD-F-009 — scored gray on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.

Evidence summary #

No Certora, Kani, or Halmos formal verification engagement found for Axelar's gateway or AxelarAuthWeighted signature verification. Informal Systems 2023-04 performed a code audit (not a prover-based FV pass) of Cosmos GMP. Web search returned no Certora Axelar report. FV coverage for the critical AxelarAuthWeighted threshold/signature path is unconfirmed.

Sources #

GitHub
Axelar Audits - FV Coverage CheckAxelar audits README: Informal Systems 2023-04 listed as audit (not FV), no Certora listedretrieved 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 axelar factor RD-F-009 score gray collected_at 2026-05-16 21:57:49