November 16, 2023

GMX V2

GMX

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

June 15, 2023

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.

May 10, 2023

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.

April 4, 2023

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.

April 3, 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.

March 15, 2023

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.

March 7, 2023

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.

January 24, 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.

January 4, 2023

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.

December 14, 2022

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

December 7, 2022

CLSynchronicity Price Adapter

Aave

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

December 2, 2022

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.

September 16, 2022

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.

July 11, 2022

Silo Protocol

Silo

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

July 6, 2022

Compound V3 (Comet)

Compound

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

June 13, 2022

OpenZeppelin Contracts

OpenZeppelin

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

April 6, 2022

Liquid Staking Contracts

BENQI

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

April 2, 2022

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

March 3, 2022

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.

Certora Logo
logologo
Terms of UsePrivacy Policy