Stopping DeFi Bugs at Scale
Certora empowers smart contract developers to detect and prevent billion-dollar mistakes before deploying code post audits. DeFi protocols like Aave, Balancer, Compound Finance, MakerDao, Sushi, and more use Certora to protect their smart contracts from bugs.
Certora secures $50 billion dollars in DeFi using the same techniques used for safety-critical programs like avionic software. Certora’s technology is developed through two decades of academic research in formal verification and programming languages.
Certora raised a $36M series B round, led by Jump Crypto and with participation from Tiger Global, Galaxy Digital, and existing series A investors: Electric Capital, ACapital, Framework Ventures, Coinfund, Lemniscap, Coinbase, and VMware.
“While there are several commendable initiatives, none of them offer a generalized scalable approach to Web3 security,” said Saurabh Sharma, Partner and Head of Investments at Jump Crypto. “Powered by world-class experts, Certora leverages formal verification to employ a suite of scalable and robust products that offer much higher reusability and granular testing.”
Certora’s team of research pioneers & security engineers
Certora is led by Shmuel “Mooly” Sagiv, Computer Science Chair at Tel Aviv University, and a pioneer of formal verification, the research field that powers the technology behind Certora. Cetora’s team of 65 people has deep mathematical and security experience and include lecturers from universities like Cornell and the University of Washington and security engineers from traditional financial firms such as JPMorgan.
How Certora works: Sushiswap’s pool-draining vulnerability caught by Certora
Certora has detected and eliminated more than 100 bugs in DeFi smart contracts. Certora works by identifying violations of “invariants” — rules that should not be broken. For example, Certora found a critical bug and prevented a pool-draining vulnerability in Sushiswap’s Trident contract.
Trident implements a liquidity pool. In a liquidity pool, users called liquidity providers add funds to create a market. In exchange for providing their funds, they earn fees from swapping activities in the pool proportional to their share of the total liquidity.
As long as there are funds in the pool, then LP shares should exist because someone is providing liquidity for this pool. This is an example of an invariant, or a rule that should not be broken in a liquidity pool.
If this invariant is violated, then there are either shares that are worth nothing or funds that cannot be claimed. In other words, either both liquidity and LP shares are zero, or none are zero.
Certora searches for scenarios that violate this invariant. This is done without creating and testing all possible scenarios. In fact, there may be infinite scenarios to try, which would make it impossible to test in this way. Instead, Certora has created a Prover that can find and display violations of invariants or formally prove that there are no violations.
In Sushiswap’s Trident contract, the Certora Prover found a violation of the invariant just before the code was deployed. This violation allowed an attacker to drain the funds in the pool. The bug was fixed before deployment, removing this attack vector (see the figure above). You can read more about the exploit here: https://medium.com/certora/exploiting-an-invariant-break-how-we-found-a-pool-draining-bug-in-sushiswaps-trident-585bd98a4d4f
Move fast and break nothing: Use Certora as a complement to human audits and bug bounties
Certora offers this technology as a tool all smart contract developers can use. Certora enables contract developers to “move fast and break nothing”, taking months off the time to market by decreasing code audit time and making it more secure. It finds bugs undetected by the best auditors, especially in complex cases when the code includes many corner cases and when contracts interact with other contracts.
Certora has prevented catastrophic bugs that human auditors missed. Certora plugs into a normal deployment pipeline. Teams use Certora after code audits are complete as a final checkpoint before launch.
Certora has prevented bugs in Aave, Balancer, MakerDao, and Compound Finance.
Here are some bugs that Certora found with its technology after completion of a traditional audit by the top security teams:
- Aave
In Aave V3, the Certora team started after the external audits and found a critical security issue that was fixed before the code was deployed Repaying with aTokens lack validation of health factor · Issue #265 · aave/aave-v3-core · GitHub 1.
- Compound
Compound’s V1 Price Oracle had rare assert failures https://www.certora.com/wp-content/uploads/2022/05/CompoundV1PriceOracleVerificationReport.pdf. This bug was identified after a complete audit, just before the protocol launched.
- Balancer
OpenZeppelin and Trail of Bits audited Balancer V2. The Certora Prover then identified a solvency bug in flash loan functionality Formal Verification helps finding insolvency bugs — Balancer V2 Bug Report | by Uri Kirstein | Certora | Medium 1. This bug was fixed before the code was deployed.
Read more about the bugs Certora has identified here: https://www.certora.com/#Reports
Certora already strengthened the security of many interesting DeFi protocols. Here are some testimonials from a few of them:
- Stani Kulechov, CEO & Founder, Aave: “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.”
- Kurt Barry, Protocol Engineer, MakerDao: “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.”
- Jared Flatow, VP of Engineering, Compound Finance: “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.”
- Matt Shams, CEO, Blockswap Labs: “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.”
- Will Papper, Co-founder and CTO, Syndicate: “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.”
- Yuchen Lin, Lead Security Engineer, TrustToken: “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.”
- Jeff Wu, CTO and Co-founder, Notational Finance: “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.”
- Fernando Martinelli, Co-founder & CEO, Balancer: “Certora has been a crucial partner along Balancer’s journey to ensure excellence in our code quality/security”
Try it out
The Certora demo is available here: https://demo.certora.com/. You can cut and paste your code or work with our example smart contracts. The full version of the tool handles multiple contracts. If you want to learn more about the technology implemented in Certora Prover please read https://hackmd.io/NxRx5e_yTNeibNle5J2yNw
We’re hiring!
Technical Roles: If you are a geek of logic, compilers, programming language design, financial math, or developer tools — we want to hear from you. Certora is looking for full-time Developers to join the Compilers, Web, DevOps, and Security teams and make formal verification a standard in the industry in Smart contracts and beyond. We want to expand our tools to other blockchains, including Web Assembly based chains such as Polkadot.
Non-Technical Roles: Certora is looking for business, community, and PR experts to make formal methods a standard practice in DeFi and beyond.
We are completely global and offer unlimited vacation, good healthcare, and 401k with matching conditions for US employees. To apply, email aviva@certora.com
