Formal verification coverage

Evidence summary #

Certora produced 2 formal verification reports (certora-boring-vault-0.pdf and certora-boring-vault-1.pdf) for BoringVault versions 0 and 1, stored in the audit directory. Exact invariant coverage percentage is not determinable from publicly accessible metadata (PDFs are binary, not parsed). Two Certora engagements indicates significant FV investment but specific coverage % is unconfirmed. Yellow: FV exists but coverage % cannot be verified.

Sources #

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 →