Formal Verification

Morpho follows a multi-faceted approach to security. Morpho security practices include formal verification, mutation tests, fuzzing, unit testing, and peer reviews that can be found within the respective GitHub repositories. External measures include professional security reviews, contests, and pre/post-deployment bounties.

To learn more, read Securing Morpho Midnight.

Formal verification using Certora

Certora is a leading formal verification platform that helps mathematically verify the correctness and security of smart contracts. Using the Certora Prover, developers define rules and invariants that are checked against the contract's code. Unlike traditional testing, Certora verifies properties across possible execution paths, helping uncover subtle vulnerabilities and prove that key security properties hold. Morpho extensively uses Certora to formally verify core protocol components, complementing its broader security practices.

Formally verified components

The full list of formal verifications is available below.