Euler Vault Kit

Euler Finance

This document describes the findings of the Euler Vault Kit project using the Certora Prover and manual code review. The work was undertaken from March 7th 2024 to May 8th 2024.

Uniswap V4 Core

Uniswap

This document describes the specification and verification of the UniswapV4-core using the Certora Prover and manual code review findings. The work was undertaken from May 28th to July 2nd, 2024.

Symbiotic Shared Security Protocol

Symbiotic

This document describes the specification and verification of Symbiotic Shared Security Protocol using the Certora Prover and manual code review findings. The work was undertaken from August 12, 2024, to September 2, 2024.

EigenLayer PEPE

EigenLayer

This document describes the specification and verification of Eigenlayer using the Certora Prover and manual code review findings. The work was undertaken from July 9th 2024 to august 12th 2024

Huma Protocol

Huma

This report describes the manual code review findings of the new Huma protocol. The work was undertaken from June 5th 2024 to July 4th 2024.

Warp Exchange

Warp Exchange

This document describes the specification and verification of the Warp Exchange using the Certora Prover and manual code review findings. The work was undertaken from April 10th to May 30th 2024.

Slender

Slender

This report describes the manual code review findings for the new Slender protocol. The work was undertaken from April 15th 2024 to May 22nd 2024.

ParaSwap Augustus V6

ParaSwap

This document describes the specification and verification of the Paraswap-Augustus using the Certora Prover and manual code review findings. The work was undertaken from 14 April 2024 to 22 May 2024.

Kinto Core & Account Abstraction

Kinto

Kinto is an L2 optimistic rollup which provides KYC, insurance, and AML & fraud monitoring at the blockchain level.

Soroban Platform

Cables

The purpose of this research was to audit all components of the Cables protocol, with the goal of validating the architecture and design, and strengthening any assumptions of soundness, security and robustness of the DeFi application.

Tokemak v2 LMPStrategy

Tokemak

This report describes the specification and verification of the Tokemak v2 LMPStrategy contract using the Certora Prover and manual code review findings. The work was undertaken from January 2nd 2023 to February 5th 2024.

Seamless ILM

Seamless

This report describes the specification and verification of the Integrated Liquidity Market (ILM) using the Certora Prover and manual code review findings. The main work was undertaken from January 28th 2024 to February 29th 2024, with an additional 3 days (March 25-28) for fix review.

Coinbase Wallet

Coinbase

This report describes the specification and verification of the Coinbase smart-account using the Certora Prover and manual code review findings.

Hyperdrive

DELV

This report describes the specification and verification of the new DELV Hyperdrive protocol using the Certora Prover and manual code review findings. The work was undertaken from May 3rd 2023 to July 1st 2023.

VE8020-Launchpad

Protofire

This report describes the specification and verification of the ve8020-Launchpad using the Certora Prover and manual code review findings. The work was undertaken from 27th November 2023 to 15th December 2023.

Blend Protocol

Blend

Blend is a lending protocol implemented on Soroban, which implements the logic for several components of a liquidity pool - namely an emitter, responsible for the generation of rewards in the form of BLND tokens, liquidity pool instances, and a backstop which provides insurance for the liquidity pools.

Ajna Protocol

Ajna

This report describes the specification and verification of the Ajna Protocol using the Certora Prover and manual code review findings.

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.