Formal verification coverage
BENQI's assessment for RD-F-009 — scored yellow on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.
Evidence summary #
Certora performed formal verification of StakedAvax.sol (sAVAX) April 2022, proving the implementation correct with respect to formal rules on critical invariants. A second Certora engagement (June 2022) verified sAVAX for Aave V3 listing. This covers the sAVAX component. The core lending Comptroller/qiToken markets have no formal verification — only traditional audit coverage. Protocol has two major risk surfaces; formal verification covers one (sAVAX) but not the other (lending). Yellow: partial FV coverage (~50% of risk surfaces formally verified).
Sources #
- AuditCertora BENQI sAVAX Formal VerificationCertora formal verification of StakedAvax.sol — April 2022; invariants proved correctretrieved 2026-05-16
- Certora Aave V3 sAVAX Listing AuditCertora Aave V3 sAVAX listing stewards audit — June 2022retrieved 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 →