Certora Prover and CVL Examples

This repository contains a collection of examples illustrating CVL usage. The specifications are compatible with CVL2.

For a reference manual and full user guide for the Certora Prover, please visit https://docs.certora.com.

Adding some below that are available in project repositories:

Openzeppelin contracts

https://github.com/OpenZeppelin/openzeppelin-contracts/tree/master/certora

Aave labs

aave v3 core

https://github.com/aave/aave-v3-core/tree/master/certora

Gho core

https://github.com/aave/gho-core/tree/main/certora

Governance crosschain bridges

https://github.com/aave/governance-crosschain-bridges/tree/master/certora

MakerDAO

DSS-allocator

https://github.com/makerdao/dss-allocator/tree/dev/certora

Lido Finance

https://github.com/lidofinance/lido-dao/tree/certoraCVL2/certora

Morpholabs

Morpho Blue

https://github.com/morpho-org/morpho-blue/tree/main/certora

Metamorpho

https://github.com/morpho-org/metamorpho/tree/certora/dev

Eigenlayer

https://github.com/Layr-Labs/eigenlayer-contracts/tree/m2-mainnet/certora

OpenSea-Seaport

https://github.com/Certora/OpenSea-seaport/tree/main/certora

Safe Ecosystem contracts

https://github.com/safe-global/safe-contracts/tree/main/certora

Ethereum Credit Guild

https://github.com/volt-protocol/ethereum-credit-guild/tree/main/certora

Raft-Fi

https://github.com/raft-fi/contracts/tree/master/certora

(Check out this webinar by Certora regarding Raft-Fi specs https://www.youtube.com/watch?v=PjUua2Hi1GA)

MZero-Labs

https://github.com/MZero-Labs/protocol/tree/main/certora

Note: Most of these projects are in active development and it is better to check the branches of the repositories for the latest versions.