Texture 2.0
This document describes the specification and verification of the SuperLendy Lending protocol using manual code review and Certora Prover. The work was undertaken from October 14, 2024, to November 22, 2024.
Mayan
The Certora audited Mayan protocol, conducted from March 3rd to March 10th, 2025, provides an in-depth specification review and manual code assessment of the FastMCTP contract.
Squads
This document describes the specification and verification of Squads using the Certora Prover and manual code review findings. The work was undertaken from Jan 7 to Jan 28, 2025
Silo
This document is a supplementary report to Certora's comprehensive smart contract audit report. The verification took place between November 4th and November 25th, 2024. Please review the primary audit report first to understand the findings discussed here.
Lido
This document describes the specification and verification of Lido Dual Governance using the Certora Prover and manual code review findings. The work was undertaken from January 10 to February 7, 2025
Lido Dual Governance
This review aims to identify potential risks within the proposed Dual Governance design. By exposing unexplored vulnerabilities, we hope to enable the Lido team to adjust the design and mitigate these risks accordingly.
MoviePass
This document describes the manual code review of the MoviePass Exchange repository (msx-smart-contract). The work took 2.5 days from 10/02/2025 to 13/02/2025. The team performed a manual audit of all the smart contracts. During the manual audit, the Certora team discovered bugs in the code, as listed on the following page.
Balancer
This document describes the verification of the Liquidity Bootstrap Pool using manual code review. The work was undertaken from 10 February 2025 to 17 February 2025. The Certora team discovered issues in the Solidity contracts code during the manual audit, as listed on the following page.
Jito
This document describes the verification effort of the Jito Tip Router using manual code review. The work was undertaken from December 23, 2024, to January 13, 2025.
EigenLayer
This document describes the specification and verification of EigenLayer Slashing using the Certora Prover. The work was undertaken from January 10th 2025 to February 11th 2025.
Kamino Finance
This document describes the specification and verification of the Kamino Lending Protocol using the Certora Prover and the manual code review of two consecutive audits. The work was undertaken from November 4, 2024 to December 13, 2024, as well as from February 3, 2025 to February 21, 2025
Balancer
This document describes the specification and verification of MEV Tax Hook using the Certora Prover and manual code review findings. The work was undertaken from 3 February 2025 to 7 February 2025.
Relend Network
This document describes the security assessment of Relend Network using manual code review findings. The work was undertaken from 3 Feb to 7 Feb 2025
Glow Finance
This document describes the findings of the manual review of Glow LRT, which was undertaken from December 2 to December 6, 2024.
Doppler
This document describes the manual smart contract security review the Cerotra team conducted from November 4 to November 11, 2024.
Lulo
This document describes the findings discovered during the audit of Lulo smart contracts using manual code review, which was undertaken from 18 November 2024 to 23 January 2025.
Balancer
This document describes the verication of Balancer V3 Stablepool Surge hook manual code review. The work was undertaken from January 23rd 2025 to January 30th 2025.
Lido
This document describes the specification and verification of Lido Dual Governance using the Certora Prover and manual code review findings. The work was undertaken from August 8 to September 5, 2024
Blend
This document describes the formal verification effort of Blend V1 using Certora’s Sunbeam Prover, a tool developed to verify Soroban smart contracts.
Veda Labs
This report presents the smart contract security audit of the Boring Bridge Holder, including manual code review findings for Solana contracts. Conducted in November 2024, the audit identified critical risks and offered insights into program authority, documentation accuracy, and decentralization concerns.
Origin Protocol
This document describes the specification and verification of Origin-Dollar using the Certora Prover. The work was undertaken from Nov 26th 2024 to Dec 12th 2024.
Silo
This document describes the specification and verification of silo contracts v2 using the Certora Prover and manual code review findings. The work was undertaken from November 4th to November 25th 2024
Balancer
This document describes the smart contract security review of Gyroscope Pools using the Certora Prover and manual code review findings. The work was undertaken from December 12th, 2024 to December 24th, 2024
Aquarius
This report describes the manual code review findings of the new Aquarius protocol. The work was undertaken from November 18, 2024 to December 13, 2024
Jito Foundation
Comprehensive security assessment and formal verification of the Stake Deposit Interceptor using manual code review and Certora Prover, conducted from November 24, 2024, to December 13, 2024.
Bold
This document describes the specification and verification of BOLD using the Certora Prover. The work was undertaken from September 9, 2024 to November 22, 2024.
Squads
This document describes the specification and verification of Squads V4 using the Certora Prover and manual code review findings. The work was undertaken from September 3 to October 1.
Frax
This document describes the specification and verification of Frax Bamm using the Certora Prover and manual code review findings. The work was undertaken from 2024-09-30 to 2024-10-21.
Sonic Labs
This document describes the specification and verification of Sonic Bridge using the Certora Prover and manual code review findings. The work was undertaken from 26/9/2024 to 14/10/2024
Manifest
This document describes the specification and verification of Manifest smart contracts using the Certora Prover and manual code review findings. The work was undertaken from 28 August 2024 to 21 November 2024.
Glow Finance
Explore our detailed manual audit of Glow V1’s Solana smart contracts, identifying vulnerabilities and providing actionable security recommendations
Balancer
This document describes the specification and verification of Balancer V3 using the Certora Prover and manual code review findings. The work was undertaken from August 6th 2024 to September 19th 2024. All contracts in the balancer-v3-monorepo are considered in scope.
Liquid Collective
This document describes the specification and verification of the Liquid Collective Liquid Staking protocol using the Certora Prover and manual code review findings. The work was undertaken from 3 December 2023 to 8 February 2024
Fragmetric
This document describes the specification and verification of Fragmetric using the Certora Prover and manual code review findings. The work was undertaken from Oct 7, 2024 to Oct 21, 2024
Jito Restaking-V2
The security assessment of Jito Restaking identifies 5 high, 3 medium, and 2 low-severity issues, including zero supply risks, unstacking logic flaws, and token validation gaps.
Reflector DAO
This document describes the specification and verification of the Reflector DAO Contract and Reflector Subscription Contract using manual code review. The work was undertaken from September 25, 2024, to October 10, 2024.
Jito Restaking
Security assessment of Jito Restaking covering high and medium-severity issues, including token denomination mismatches, vault update delays, fee inaccuracies, and overflow risks. Conducted from Aug 8 – Sep 19, 2024.
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.
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.
Solana Foundation
This document describes the specification and verification of the Token Extensions using the Certora Prover. The work was undertaken from 02/01/2024 to 05/15/2024.
Tether
This document describes the specification and verification of the TetherToken using the Certora Prover and manual code review findings. The work was undertaken from 19 February 2024 to 29 February 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.
Curve Security
Curve Security Analysis Report and Formal Verification Properties
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.
Compound
We analyzed two versions of the code, verifying 5 global properties, uncovering 7 issues, and confirming the resolution of 1 issue between versions across the CarefulMath, Exponential, and PriceOracle contracts.