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
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
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
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
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
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
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
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
Kinto is an L2 optimistic rollup which provides KYC, insurance, and AML & fraud monitoring at the blockchain level.
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
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
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
This report describes the specification and verification of the Coinbase smart-account using the Certora Prover and manual code review findings.
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.
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
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
This report describes the specification and verification of the Ajna Protocol using the Certora Prover and manual code review findings.
GMX
This report describes the specification and verification of GMX V2 protocol using the Certora Prover and manual code review findings.
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.
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.
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
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
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.
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.
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
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.
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
Aave
The Certora team manually reviewed five Aave contracts, including CLSynchronicityPriceAdapterBaseToPeg.sol, CLSynchronicityPriceAdapterPegToBase.sol, CLwstETHSynchronicityPriceAdapter.sol, ProposalPayloadStablecoinsPriceAdapter.sol and ArcProposalPayloadStablecoinsPriceAdapter.sol
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.
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
This document describes the specification and verification of Silo’s protocol using the Certora Prover.
Compound
This document describes the specification and verification of Silo’s protocol using the Certora Prover.
OpenZeppelin
This report describes the specification and verification of OpenZeppelin's contracts using the Certora Prover.
BENQI
This document describes the specification and verification of BENQI's Liquid Staking system using the Certora Prover.
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
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.