We’ve been working on a compiler equivalence checker. Given two programs, our checker uses the existing Certora Prover infrastructure to prove that the programs are equivalent on all inputs.
June 30
Ensuring Fair Redemptions in infiniFi with Formal Verification
We’ve been working on a compiler equivalence checker. Given two programs, our checker uses the existing Certora Prover infrastructure to prove that the programs are equivalent on all inputs.
On June 25th, the Silo team informed us that an incident occurred in which overly broad approvals inadvertently enabled a borrow manipulation exploit. Importantly, this module is entirely separated from the core Silo contracts - no vaults, markets, or user funds were affected or at risk.
This blog post demonstrates how formal verification with Certora Prover complements traditional fuzz testing by identifying critical edge cases in Uniswap v4. By translating fuzz tests into robust Certora Verification Language (CVL) rules, our approach uncovered subtle vulnerabilities, particularly involving malicious hooks
The Ethereum Object Format (EOF) proposal removes dynamic jumps to make smart contract bytecode more predictable and analyzable. Some critics argue that easier static analysis offers limited value, but we disagree. Static analysis tools have already prevented countless costly bugs. Simplifying EVM control flow could pave the way for safer contracts and better tooling. Security must be a central factor when shaping Ethereum’s future.
Formal verification is the only tech that proves your code works as intended, across all inputs. As bugs continue to drain millions from Web3 apps, formal methods offer strong, mathematical guarantees. Learn why DeFi and critical smart contracts can't afford to skip it anymore.
In recent years, tiny rounding mistakes, often as small as 1 wei, have cost DeFi protocols over $100 million. Because the EVM only handles integers, every division forces a round‑up or round‑down decision, creating subtle gaps that attackers can exploit at scale. Learn how formal verification tools can systematically prove your contracts’ invariants and reveal hidden rounding bugs before they go live.
Kamino Lending partnered with Certora's formal verification to identify and resolve a subtle rounding issue in its Solana-based lending protocol, proactively securing it against potential future exploits.
This article explores the formal proof of solvency in Uniswap v4, ensuring that Automated Market Makers (AMMs) always have enough funds to cover withdrawals. By leveraging mathematical invariants, SMT solvers, and precise token accounting, we demonstrate how Uniswap v4 maintains security and solvency.
Certora has open-sourced the Certora Prover, the most advanced formal verification tool for smart contracts on Ethereum, Solana, and Stellar. Used to secure over $75B in DeFi assets, the Prover guarantees correctness by detecting all potential bugs. Start verifying your code today!
Certora is a leading provider of technology and services for eliminating vulnerabilities in smart contracts. This white paper outlines the technology that makes Certora unique, explaining both its power and its current limitations.
The Bybit breach targeted its Ethereum (ETH) multisig cold wallet—a storage system touted as ultra-secure. This wasn’t a brute-force attack or a flaw in the blockchain itself; instead, it was a sophisticated operation that exploited human trust and operational weaknesses. For anyone using or considering a multisig wallet—whether you’re a crypto enthusiast, a startup founder, or a business managing digital assets—this incident is a wake-up call. Let’s break down what happened and what you can do to keep your funds safe.
Safeguard is a Geth extension that monitors Ethereum protocol invariants in real time to enhance the security of DeFi systems and monitor exploits.
Lido Finance, a leader in liquid staking, recently introduced a dual governance system to protect user funds and boost DAO security. However, any innovation carries risks and bugs in Lido’s governance would ripple across DeFi. This post details the design review process for Lido's governance system, outlining the challenges, bugs discovered, and solutions implemented to ensure the security and robustness of the protocol.
Learn the best practices for writing secure Uniswap v4 hooks to prevent vulnerabilities and enhance DeFi security. Follow expert guidelines to safeguard your smart contracts.
Learn how Certora’s formal verification secures Uniswap v4, ensuring the safety of billions in user funds through mathematical proofs and advanced security measures.
Explore Quorum, the open-source tool protecting Aave, that secures DAO governance by automating verification, detecting risks, and ensuring proposals execute as intended.
Discover critical security findings from Uniswap v4’s audits by Certora, OpenZeppelin, Trail of Bits, and Spearbit. Learn how vulnerabilities like double counting on CELO and tick price invariant violations were uncovered and mitigated to strengthen DeFi security.
Certora’s rigorous audit and formal verification strengthened Symbiotic’s protocol, addressing issues and ensuring secure mainnet deployment.
Explore Uniswap v4's innovative features and the associated security challenges. Learn how threat modeling identifies attack vectors and safeguards DeFi protocols.
Discover how formal verification caught a sneaky vulnerability in integration of Ethereum's upcoming Electra upgrade that slipped past traditional audits, and what it means for one of crypto's hottest protocols.
Smart contracts are designed to carry out financial transactions involving millions of dollars. Bugs in these programs are known to have severe consequences. Naturally, formal verification plays a critical role in this domain. In this blog, we present Certora’s recent efforts towards formally verifying Wasm bytecode.
During Aave V3’s deployment on ZKsync, a severe LLVM compiler bug was discovered—one that could lead to fund loss. Learn how Certora, Aave Labs, BGD Labs, and Matter Labs traced the issue to its root cause and uncovered a hidden risk in compiler optimizations.
Certora recently raised the bar for DeFi security by formally verifying a key property of the Euler V2 Vault implementation. In this post we talk about how formal verification can offer strong assurance about DeFi protocols, find rare bugs unknown to developers, and even involve specifications that are simpler to understand than exploits.
The Certora team recently finished reviewing token extensions on Solana utilizing our in-depth formal verification tools.
This article is for students with a math or computer science background interested in learning more about decentralized finance (DeFi), developing analytical skills, and earning lucrative income by helping secure software.
Formal verification contests offer a measurable and effective approach to increasing code security by combining the depth of formal verification with the breadth of the community. Learn how you can leverage formal verification to get better results from audit competitions.
Prover version 7.3.0 is out! This update aims to enhance your user experience and address some minor bugs reported by our users.
Certora today announced its engagement with Solana Foundation to review and formally verify the code underlying token extensions on Solana, the new program-level token features that natively extend token functionality.
In this post (the sequel to “How to optimize your gas consumption without getting REKT”), we focus our attention on Solidity/Yul libraries that realize the mathematical and economic computations that lie at the heart of the DeFi world, and explain why equivalence checking is a potent tool in the hands of developers and auditors who wish to work on such code.
AAVE started in 2017, which in the world of DeFi, a domain that has been popular since only 2017, is considered OG. Aave, or in its former name ETHLend, started as a P2P lending protocol, but later transformed into a liquidity pool-based protocol in early 2020. Back then, Certora, a small company with major talent and advanced-yet-unripe technology, aspired to enhance the security of an innovative protocol that prioritizes safeguarding against breaches.
In the previous post, we showed how to prove the correctness of Mint operation which is part of the basic functionality of both the SPL Token. In this post, we show how the Solana Certora Prover (SCP) can be used to find bugs in the confidentiality extension of the SPL Token.
The Vyper programming language provides a clean memory and control abstraction. In comparison to Solidity, it is considered highly attractive for DeFi programming.
In our previous post, we described our new verification tool for Solana contracts. In this post, we show the verifier in action on SPL Token 2022, a widely-used Solana application. In the next post, we will show how to find bugs in the confidential extension of SPL Token 2022.
In a series of posts, we shall discuss our efforts to formally verify Solana smart contracts. We have developed a new in-house verification tool that takes Solana contracts written in Rust together with a specification and automatically proves that the specification holds.
The first time that an automatic tool has found a bug in a public, open-source, Solidity library.
On May 10th, the Silo team informed us about a critical vulnerability that had been reported by an external researcher and fixed a few days before. We conducted a thorough investigation and manual review of the issue, the fix, and the rest of the code base.
Developing a DeFi product is an engineering problem of deceptive depth — it is easy to write a smart contract in Solidity that (mostly) does what you want, but it is hard to do it well.
In this blog, we discuss our efforts to apply mutation testing in the context of automated verification.
Formal verification uses mathematical models and computer algorithms to prove or disprove the correctness of the system’s design with respect to formal specifications expressed as properties.
Formal verification improves software security by finding bugs and mathematically proving their absence via mathematical methods. Smart contracts are perfect applications for formal verification because bugs are costly, the code is typically small or modular, and it evolves over time.
Certora identified and disclosed a significant optimization bug affecting Solidity compiler versions ≤0.8.14, where crucial memory operations in inline assembly could be erroneously removed, potentially impacting smart contract correctness.
Certora uncovered a Solidity compiler bug affecting inter-contract calldata validation in versions ≤0.8.13. The bug allowed malicious inputs to corrupt external calls, posing serious security risks.
This blog details the discovery of a critical pool-draining vulnerability in SushiSwap’s Trident protocol. By establishing a key invariant and using automated formal verification, researchers uncovered a flaw in the burn-single operation that could have allowed an attacker to drain liquidity.
This blog post revisits the infamous Popsicle Finance bug, which resulted in a $20MM loss by exploiting a flaw in the token transfer mechanism. Using the Certora Prover for formal verification, we explain how the error—in which the transfer function failed to update profit-tracking variables—allowed attackers to boost a collaborator’s profit share illegitimately.
Certora uncovered a severe Solidity compiler bug (≤0.8.3) allowing maliciously crafted byte buffers to violate memory isolation during ABI deserialization. This vulnerability enabled attackers to access unintended memory regions or inject non-deterministic behavior into smart contracts.
Certora uncovered a serious Solidity bug (fixed in v0.8.0) where maliciously crafted storage fields could exploit abi.encodePacked, causing unexpected memory exposure and non-determinism in Ethereum smart contract transactions.
Certora identified a serious bug in Solidity compiler 0.7.3 silently corrupting storage when handling zero-length bytes arrays, resulting in increased gas costs and potential data inconsistencies.
Certora discovered a critical Solidity compiler bug (fixed in 0.6.5) enabling memory corruption through overflow in dynamically sized arrays. Understand the bug’s details and impact.
