“Certora’s technology helped to cover security on decentralized Aave Protocol, essentially finding vulnerabilities that are usually difficult to find in manual code reviews and audits. When building mission-critical software such as financial technology, Certora is a must.”
“Formal verification from Certora is the most powerful tool we have to ensure that we are building a secure, impenetrable system -- the top priority for any serious smart contract developer."
“Certora has been a crucial partner along Balancer's journey to ensure excellence in our code quality/security"
“Certora has been a critical security partner in Stakehouse Protocol’s formalization efforts. We are consistently impressed by the team’s hands-on approach and their Certora Prover tool efficacy. It reinforces the key mechanisms while giving clarity and adversarial simulation for our Multichain ETH scenarios.”
"Certora gives us so much peace of mind as we develop smart contracts at Syndicate. With formal verification running on every single commit, we can maintain a fast development velocity without decreasing security."
“Certora has unlocked TrustToken’s ability to iterate quickly while maintaining confidence in the security of our smart contracts. Our team has discovered and fixed numerous unintended bugs thanks to this powerful tool.”
"Certora has given us the ability to practically apply formal verification methods to anything we do on-chain. They have an excellent team who we've partnered with closely over the years, and the process of writing invariants with them has proven to be invaluable in writing better smart contracts."
“The Certora prover plays an important role in our overall safety strategy by providing an accessible way to quickly iterate on formal specifications and determine the correctness of bytecode. It's what we reach for when both time and safety are of the essence. Engineers can learn to use it in a few days and don't need a Ph.D. in formal methods to create good specifications. The tool recently helped us to uncover an inconsistency in an updated version of one of our oldest smart contracts, which was a surprising result. The Certora team is highly responsive and promptly addresses issues we encounter.”
MakerDAO enables the generation of Dai, the world’s first unbiased currency and leading decentralized stablecoin. Dai is a stable, decentralized currency that does not discriminate. Any individual or business can realize the advantages of digital money.
Syndicate enables scalable on-chain infrastructure and is backed by a16z, IDEO CoLab Ventures, Variant, Electric Capital, and over 100 other investors and strategic partners.
Balancer is a protocol for programmable liquidity. It allows for the creation of self-balancing liquidity pools with flexible parameters. A pool can have 2 or more tokens and each token can have different weights. Balancer also allows for smart pools which have evolving parameters: think of a surge pricing liquidity pool that increases the trading fees in times of high volatility/demand for liquidity.
Aave Protocol is a decentralized, open-source, and non-custodial money market protocol. Depositors can deposit assets into the protocol and earn interest on their deposits without relying on middlemen.
Compound is a transparent, autonomous money market — allowing users & applications to frictionlessly earn interest or borrow Ethereum assets without relying on a counterparty.
Silo is a risk-isolating lending protocol that implements permissionless lending markets where any token can borrow another. Silo is secure by design – each lending market supports two assets only, the bridge asset and a unique token asset. This design concentrates liquidity in single pools and allows for efficiency.
Morpho is a Peer-to-Peer (P2P) layer on top of lending pools like Compound or Aave. Rates are seamlessly improved for both suppliers and borrowers whilst preserving the same liquidity and market risk guarantees.
✓ Balancer’s Timelock Authorizer Verification Report, May 2023.
✓ Aave Static aToken, April 2023.
✓ Aave V3 PR #820, March 2023.
✓ Aave GHO Stablecoin, March 2023.
✓ Aave Staked Token v1.5, February 2023.
✓ Radicle Drips, January 2023.
✓ Aave CLSynchronicity Price Adapter, December 2022.
✓ Aave Proof of Reserve, November 2022.
✓ Aave-StarkNet L1-L2 Bridge, October 2022.
✓ Aave V3 BTC.b Listing Steward, September 2022.
✓ AAVE Token V3, September 2022.
✓ Aave Governance V2 Update, September 2022.
✓ Aave V3 sUSD Listing Steward, August 2022.
✓ Aave V2 AStETH, August 2022.
✓ Aave V3 sAVAX Listing Steward, July 2022.
✓ Aave V3 MAI & FRAX Listing Stewards, August 2022.
✓ SaaS Verification Report by Blockswap Labs July 2022.
✓ SaaS Verification Report by Silo July 2022.
✓ Compound V3 Comet Verification Report, July 2022.
✓ Benqi’s Liquid Staking Contracts, April 2022.
✓ OpenZeppelin Governance contracts, December 2021.
✓ SushiSwap ConstantProductPool, November 2021.
✓ SushiSwap TridentRouter, November 2021.
✓ Popsicle V3 Optimizer, November 2021.
✓ Notional Finance V2, November 2021.
✓ Celo Core Contracts Release 4, May 2021.
✓ Sushi Compound Strategy, April 2021.
✓ Balancer V2 (Issues only), April 2021.
✓ Kashi Lending Protocol, March 2021.
✓ dForce Lending Protocol, February 2021.
✓ Origin OUSD Token, February 2021.
✓ Sushi BentoBox, February 2021.
✓ Opyn Gamma Protocol, December 2020.
✓ Synthetix Multi-Collateral Loans, December 2020.
✓ Aave Protocol V2, December 2020.
✓ Keep’s Fully-backed bonding contract, November 2020.
✓ Compound’s Open-Oracle with Uniswap Anchor, August 2020.
✓ Celo Governance Protocol, May 2020.
✓ Orchid’s Smart Contracts, December 2019.
✓ Compound’s MoneyMarket v2 formal verification report, August 2019.
✓ To learn how to use the Certora Prover, see our Quick guide.
✓ In our webinars, Dr. James Wilcox presents the basics of Formal Verification and shows the Certora Prover in action, and Prof. Mooly Sagiv explains the technology underlying the Certora Prover.
✓ New Tech for Smart Contract Security by Professor Daniel Jackson, MIT
✓ Our SBC paper describes how generic rules can be used to find bugs.
✓ Our OOPSLA'2020 paper presents the most precise way for proving a code is immune to reentrancy-style attacks. (Video)
.svg)
.png)
.png)
US / Europe
Certora offers a unique SaaS product called the Certora Prover for Web3 code security. The Certora Prover compares the smart contract code to a formal specification – a way to express fundamental properties of the code. The tool automatically locates bugs before deployment or mathematically proves their absence even after contract updates. The Prover plugs into your standard deployment pipeline and is an essential complement to human audits and bug bounties. Notice that, unlike manual audits, the tool is immediately available and can be applied.
This is exactly the intended use case of the Certora prover!
The Certora Prover provides complete path coverage for a set of safety rules provided by the user. For example, a rule might check that only a bounded number of tokens can be minted in an ERC20 contract. The prover either guarantees that a rule holds on all paths and all inputs or produces a test input that demonstrates a violation of the rule.
The problem addressed by the Certora Prover is known to be undecidable. This means that there will always be pathological programs and rules for which the Certora prover will time out without a definitive answer. Our experience so far is that realistic customer’s programs are not pathological and can be successfully analyzed by the Prover. The Certora team is actively working to reduce the number of timeouts when analyzing smart contracts of customers.
A traditional security audit usually involves a manual, holistic review of an entire system. Formal verification, on the other hand, produces a proof that a piece of software satisfies a specification. The Certora team is available for formal verification projects to write specifications and verify the code against these specifications. Often, verification projects find bugs in the code, and these bugs can be fixed during the course of the project, with the fixes proved correct. The team also produces a report describing the properties verified and bugs discovered. At the moment, we only analyze and review Ethereum bytecode.
Definitely, and we will assist you and review your rules for free.
The Certora Prover takes as input the smart contract (either as EVM bytecode or Solidity source code) and a set of rules, written in Certora’s specification language. The Prover then automatically determines whether or not the contract satisfies all the rules. Just as good testing sometimes requires code refactoring, verification occasionally requires changes to the code. For example, because the verification happens via the public API to the contract, some state pieces may need to have getters added so that they are accessible.
When the Certora Prover provides a test input that violates the rule, the user can check if this violation is due to a bug in the code or the verification rule. We also suggest performing a sanity check on the rules, e.g., by mutating the contract by adding an artificial bug and checking if any rule is violated. If no violations were found, the specification is missing a rule. The Certora Prover also automatically generates test cases for showing that a point in the program is reachable.
The Certora prover currently analyzes EVM bytecode combining two computer science techniques: abstract interpretation and constraint solving. These are well understood academic fields.
Unlike symbolic execution tools which select specific paths and a fixed set of bad patterns, such as MythX and Slither, the Certora Prover provides complete coverage for a user provided set of rules. Interactive theorem provers such as Coq and K can be used for interactively showing that a specific contract is correct. SMTChecker by the Solidity team and Verisol by Microsoft Research are similar to the Certora Prover in many respects but target Solidity sources with per program user assistance. This makes the tools hard to integrate into the CI pipeline --- the value of the verification is that it allows to move fast and break nothing!
