Formal verification coverage
A code & audits factor in the v1.7.0 rubric. Measured per protocol on a s cadence.
Methodology how we score #
**What this measures** This factor records the percentage of a protocol's declared critical invariants that are covered by formal verification proofs, using tools such as Certora Prover, Kani, Halmos, or equivalent formal methods frameworks. The measurement requires the protocol to have a published list of critical invariants (e.g., 'total collateral always exceeds total debt') and at least one formal verification report referencing those invariants. The data source is the FV report and protocol documentation.
**Why it matters** Formal verification provides mathematical proof that specified properties hold across all possible inputs and state transitions -- a qualitatively different guarantee from fuzz testing or audit review. KyberSwap Elastic ($48M, 2023) lost funds to a sub-microscopic precision failure in tick-crossing arithmetic that survived multiple audit rounds; formal verification of the tick boundary invariants would have been the only method capable of detecting the specific edge case before deployment. The MonoX self-swap bug ($31.4M, 2021) similarly exploited a mathematical property that two auditors missed but that could have been caught by a formal model of the token pricing invariants. Formal verification coverage is a P2 signal -- it adds meaningful signal for complex AMMs and lending protocols but is not yet an industry baseline.
**Green / Yellow / Red** Green: at least 80% of the protocol's declared critical invariants have formal verification proofs attached to the currently deployed code. Yellow: formal verification exists but covers less than 80% of declared critical invariants, or covers a prior code version rather than the currently deployed bytecode. Red: no formal verification of any kind exists for any critical invariant.
**Common gray cases** Most protocols do not publish an invariant list or commission formal verification; this factor is legitimately gray for the large majority of DeFi protocols at the current state of industry practice.
**Notable historical examples** - **KyberSwap Elastic** ($48M, 2023): Tick arithmetic precision failure that formal verification of boundary invariants would likely have detected. - **MonoX** ($31.4M, 2021): Self-swap token pricing bug; formal model of AMM price invariants could have surfaced the logical inconsistency. - **Value DeFi** ($10M, 2021): AMM math error in a complex multi-token pool. - **Bunni** ($8.4M, 2025): Complex concentrated-liquidity math without formal verification coverage.
Measurement what to look for #
Determine the percentage of protocol-declared critical invariants covered by a formal verification proof (Certora Prover, Kani, Halmos, or equivalent).