Formal verification coverage
Lombard Finance'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 #
No formal verification (Certora Prover, Kani, Halmos, or equivalent) has been performed on any Lombard EVM contracts. None of the 12+ audit reports in the GitHub directory reference formal verification. Veridise audits use static analysis and manual code review, not FV. OZ audits use Slither-family tooling and manual review. No Certora specification files found in the evm-smart-contracts repository. Per methodology: red = 0% formal verification coverage. No critical invariants formally specified or proved.
Sources #
- GitHublombard-finance/evm-smart-contracts — no FV specsNo Certora spec files found in evm-smart-contracts reporetrieved 2026-05-05
- Veridise LBTC V1 Audit PageVeridise V1: static + manual methods (not FV); Veridise V2: sameretrieved 2026-05-05
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 →