Formal Verification
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.
A whole article was dedicated to the Morpho Security Framework.
The full list of formal verifications is available below.
| Formally Proven | Scope | Tool Used |
|---|---|---|
| Morpho token | ERC20 and delegation logic | Certora |
| Morpho Blue | core logic | Certora & Halmos |
| Morpho Blue - Pre-liquidation | core logic | Certora |
| Bundler3 | core logic | Certora |
| Vault V2 | core logic | Certora |
| Midnight | core logic | Certora |
| Morpho data structures (Legacy) | double linked list and logarithmic buckets | Certora & Halmos |
| Morpho Aave V3 (Legacy) | core logic | Why3 |
| Morpho optimizers (Legacy) | Merkle tree and claim function | Certora & custom checker |
| Universal rewards distributor (Legacy) | Merkle tree and claim function | Certora & custom checker |
| Morpho token (legacy) | authorization system | Certora |
| Morpho utils (Legacy) | math functions | Certora |
| Vault V1.0 (Legacy) | core logic | Certora |