Formal verification coverage
mETH Protocol'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 #
Zero formal verification found. Certora SecurityReports GitHub index has no mETH or Mantle LSP entry. The only FV-adjacent work is an independent community project (0xpolarzero/mantle-lsp-fuzzing-formal-verification) using Halmos, covering only the Staking contract's ETH-accounting invariants — it is archived (March 2024) and explicitly self-described as 'not an assessment of the whole system.' At $535M current TVL ($2.1B historical peak) with no official FV program, this is red per U8 flag and LST-protocol precedent (Rocket Pool, StakeWise).
Sources #
- GitHubIndependent Mantle LSP Halmos fuzzing repo (community, archived)Community Halmos fuzzing/FV repo — archived Mar 2024, explicitly not a protocol assessment, incomplete Certora sectionretrieved 2026-05-16
- Certora Formal Verification Portfolio — no mETH entryCertora SecurityReports portfolio — no Mantle/mETH entry in the EVM protocol listretrieved 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 →