Formal verification coverage
Sushi (SushiSwap) — v2 + v3 + Trident + BentoBox/Kashi + SushiXSwap's assessment for RD-F-009 — scored gray on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.
Evidence summary #
Certora conducted formal verification of BentoBox (Feb 2021) per certora.com listing, but the report page rendered header-only (content inaccessible via WebFetch). Coverage percentage and specific invariants verified cannot be confirmed. No FV found for v2-core, v3-core, RouteProcessor series, or SushiXSwap. The ToB Uniswap v3 audit included Echidna + Manticore symbolic execution for the upstream codebase but this was not a Sushi-specific engagement. Coverage % cannot be computed.
Sources #
- GitHubsushiswap/v3-core ToB audit directory (Echidna/Manticore)sushiswap/v3-core/audits/tob/contracts/crytic/ — Echidna/Manticore scripts (upstream Uniswap v3, not Sushi-specific)retrieved 2026-05-17
- Certora BentoBox Formal Verification Feb 2021Certora BentoBox FV Feb 2021 — listing confirmed, content inaccessibleretrieved 2026-05-17
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 →