Mayan FastMCTP
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 Smart Account Program v0.1
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
SiloCore V2
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.
Design Review & Risk Analysis
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.
Lido Dual Governance
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
MSX Smart Contract
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.
Liquidity Bootstrap Pool
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 Tip Router
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 Protocol
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 Lending
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
MEV Tax Hook
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
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
Doppler
Doppler
This document describes the manual smart contract security review the Cerotra team conducted from November 4 to November 11, 2024.
Glow LRT
Glow Finance
This document describes the findings of the manual review of Glow LRT, which was undertaken from December 2 to December 6, 2024.
Lulo
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.
Lido Dual Governance
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
Stablepool Surge hooks
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.
Boring Bridge Holder
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 Dollar
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 v2
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
Gyroscope Pools
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 AMM Security
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
Stake Deposit Interceptor
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.
Liquity
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 v4
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.
Bamm
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 Bridge
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
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.
Balancer V3
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.
Security Assessment & Formal Verification Report
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 v1
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
Security Audit & Formal Verification
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 Security Assessment v1
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.
Security Assessment & Formal Verification
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 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.
Token 2022 Extension
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 Token Security Review
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
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.
Curve Security Analysis Report
Curve Security
Curve Security Analysis Report and Formal Verification Properties
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
Rocket Joe
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 Price Oracle
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.
