Formal verification coverage

Symbiotic'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 Prover formal verification engagement from August 12 to September 2 2024. Certora report page confirms: the Prover verified that the implementation adheres to formal specifications, and a manual review uncovered several bugs detailed in the report. FV covered Symbiotic core contracts. Specific percentage of critical invariants covered is not publicly accessible without the PDF. Scored yellow: FV presence confirmed and passed, but scope breadth unverifiable.

Sources #

Audit
Certora Symbiotic Audit and Formal Verification ReportCertora report: Prover confirmed implementation adheres to formal specifications; manual review found several bugs; engagement Aug 12 - Sep 2 2024retrieved 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 →

rubric_version v1.7.0 protocol symbiotic factor RD-F-009 score yellow collected_at 2026-05-16 09:25:24