
GMX V2
GMX
This report describes the specification and verification of GMX V2 protocol using the Certora Prover and manual code review findings.

Aave Vault
Aave
This document describes the specification and verification of Aave's Vault using the Certora Prover. The Certora Prover proved the implementation correct with respect to the formal rules written by the Certora team.

TimelockAuthorizer
Balancer
This report describes the specification and the verification of Balancer’s contract TimelockAuthorizer using the Certora Prover. The Certora Prover proved that the implementation of the contract above is correct with respect to formal specifications written by the Certora team. The team also performed a manual audit of these contracts.

Static aToken V3
Aave
This document describes the specification and verification of Aave's static aToken V3 using the Certora Prover. The work was undertaken from January 18th to March 31st, 2023.

Lido V2
Lido
This document describes the specification and verification of the new Lido V2 protocol with enabled Ethereum withdrawals and modular Staking Router architecture using the Certora Prover and manual code review findings.

Aave V3 PR #820
Aave
This change includes two updates to the current behaviour of Aave protocol v3. First, it prevents users from enabling an asset with 0 LTV as collateral. Second, when receiving an asset in isolation, it will no longer be enabled automatically as collateral, with the exception of suppliers who assign themselves with a new role called ISOLATED_COLLATERAL_SUPPLIER for which the old behaviour will still hold.

GHO Stablecoin
Aave
This document describes the specification and verification of Aave's GHO Token using the Certora Prover. The work was undertaken from the 30th of January 2023 to the 28th of February 2023.

Rescue Mission Phase 1
Aave
This document describes the specification and verification of Aave's rescue mission phase 1 using the Certora Prover. The work was undertaken from January 6th to January 12th.

Radicle Drips Contracts
Radicle Drips
This document describes the specification and verification of Radicle Drips Contracts using the Certora Prover. The work was undertaken from 06 December 2022 to 01 January 2023.

Upgrade to V3.0.1
Aave
This document describes the specification and verification of an upgrade to Aave V3 into version V3.0.1 using the Certora Prover. The new version introduces fixes that were discovered after a year of testing V3 across different networks - context. This verification project aims to enhance the existing specifications of Aave V3 core and add new properties

CLSynchronicity Price Adapter
Aave
The Certora team manually reviewed five Aave contracts, including CLSynchronicityPriceAdapterBaseToPeg.sol, CLSynchronicityPriceAdapterPegToBase.sol, CLwstETHSynchronicityPriceAdapter.sol, ProposalPayloadStablecoinsPriceAdapter.sol and ArcProposalPayloadStablecoinsPriceAdapter.sol

SidechainBridge
dcSpark
This document describes the specification and verification of the sidechain bridge of the Milkomeda protocol using the Certora Prover. The latest commit that was reviewed and run through the Certora Prover was ce5827a. The scope of our verification was the SidechainBridge contract.

Stable Pool
Balancer
This document describes the specification and verification of Balancer's contracts using the Certora Prover. The Certora Prover proved the implementation of the Balancer contracts is correct with respect to the formal rules written by the Balancer and the Certora teams.

Silo Protocol
Silo
This document describes the specification and verification of Silo’s protocol using the Certora Prover.

Compound V3 (Comet)
Compound
This document describes the specification and verification of Silo’s protocol using the Certora Prover.

OpenZeppelin Contracts
OpenZeppelin
This report describes the specification and verification of OpenZeppelin's contracts using the Certora Prover.

Liquid Staking Contracts
BENQI
This document describes the specification and verification of BENQI's Liquid Staking system using the Certora Prover.

OpenZeppelin Contracts
OpenZeppelin
This document describes the specification and verification of OpenZeppelin's contracts using the Certora Prover. The scope of this verification is OpenZeppelin's governance system

Balancer TimelockAuthorizer
Trader Joe
This document describes the specification and verification of Rocket Joe system using the Certora Prover. The scope of this verification is the Rocket Joe system.