Formal verification coverage
Falcon 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) identified in any audit or public disclosure. Zellic and Pashov use traditional manual review. No FV spec files findable.
Detail #
Neither Zellic nor Pashov employ formal verification methods — both use traditional static analysis and manual code review. No Certora specification files are findable (no public GitHub). The transparency security guide mentions custody and audit methodology but not formal verification. The protocol has not declared formal critical invariants. Methodology red threshold: 0% formal verification coverage.
Sources #
- AuditZellic Falcon Finance AuditZellic audit uses traditional methods — no FV scope statedretrieved 2026-05-12
- Falcon Finance Transparency and Security GuideFalcon Finance security guide — no formal verification mentionedretrieved 2026-05-12
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 →