Formal verification coverage

Frax Finance'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 engaged for BAMM formal verification + audit (Oct-Dec 2024): both FV (Prover) and manual review confirmed via Certora SecurityReports portfolio ('2024/12_10_2024_Frax_Bamm-FV-MR.pdf'). No FV report found for frxUSD, sfrxUSD, Fraxlend, Fraxswap, frxETH, or frxGov. BAMM-only FV = partial coverage of the 6-product umbrella. Estimated <20% of TVL-bearing contract critical invariants covered by FV. Yellow: FV exists but covers only one product module.

Sources #

Audit
Certora BAMM Audit Report FinalCertora BAMM report PDF in frax-solidity reporetrieved 2026-05-17
GitHub
Certora Security Reports PortfolioCertora SecurityReports — Frax BAMM FV+MR Dec 2024 confirmedretrieved 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 frax factor RD-F-009 score yellow collected_at 2026-05-16 20:44:31