Formal verification coverage
Chainlink CCIP'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, Kani, Halmos) engagement found for CCIP contracts. Chainlink's formal verification article claims 'formal methods are applied to core protocol components' without naming any tool, invariant set, or coverage percentage. ISO 27001 and SOC 2 Type 2 are compliance certifications, not formal verification. Per U8 methodology instruction: zero documented FV on a bridge with ~$7B value secured scores red.
Sources #
- URLFormal Verification of Smart Contracts | Chainlink (no CCIP-specific FV documented)Chainlink formal verification article — claims general FV application, no specific tool/invariant/coverageretrieved 2026-05-16
- Chainlink Security Certification PageChainlink ISO/SOC2 certifications — compliance not FVretrieved 2026-05-16
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 →