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.