What Is Formal Verification?
Formal verification checks whether code satisfies precisely stated properties within a defined model and set of assumptions. This guide explains what that means for smart contracts, how it complements testing and human audits, and what a verification engagement involves. A flaw found in Solana’s SPL Stake Pool shows how a property can expose a consequential edge case before deployment.
The Tectonic exploit combined exchange-rate manipulation with TONIC price manipulation to inflate collateral and borrow approximately $120.4M across nine markets. This analysis breaks down the exploit, the property verified by Certora Prover, and how the accounting issue can be prevented.
Certora is extending AutoProver to Rust and building native formal verification support for Solana programs. AutoProver uses AI agents to analyze code, generate candidate properties and investigate failures, while Certora’s prover determines whether those properties hold. The open-source work builds on Certora’s existing verification experience across the Solana ecosystem, with an initial release targeted around Solana Breakpoint in November 2026.
How zero-fill matching, deferred cleanup, and atomic rollback combined to disrupt order-book matching, and how Aftermath addressed it.
We formally verified memory safety for inflate_table, a 266-line function in zlib where low-level memory operations depend on subtle algorithmic invariants. Starting without an existing C-to-Lean verification pipeline, we built one and produced a ~20,000-line Lean proof of memory safety and termination. LLMs generated most of the proof, while Lean checked every step.
Certora and powdr developed a verifier that checks whether autoprecompile optimizations preserve program behavior. Across Keccak and Reth workloads, it proved more than 98% of 6,627 circuit-equivalence checks automatically.
Certora compared AutoProver’s independently generated Aave v4 Hub specification with a human-authored verification engagement. AutoProver discovered and proved substantial solvency and accounting properties, but the comparison also revealed why generated coverage must be paired with expert analysis of protocol intent and economic safety.
AutoProver utilises AI agents and formal methods to automatically infer intent from your code, generate specifications, and prove the absence of bugs.
Certora verified the security of Solana's core upgrade from SPL Token to the optimized P-Token program. We used the Certora Solana Prover to prove their equivalence, ensuring that P-Token is a safe drop-in replacement.
Certora has received a grant from the Canton Development Fund to develop a new open-source static analysis tool for Daml smart contracts on the Canton Network. The tooling will help developers and financial institutions analyze cross-package contract interactions, improve visibility into authority delegation and privacy implications, and strengthen security assurance for multi-party blockchain applications before deployment.
This article presents two complementary methodologies for threat modeling: Certora's "4 A's" framework and the STRIDE framework. Soroban smart contracts teams who invest in this essential process early will lay the groundwork for security, resulting in simpler architecture, fewer bugs, and faster audits.
We have released Certora Prover Version 8.13.0 that includes new features for EVM, Solana, and Soroban.
Cross-chain swaps depend on more than bug fixes. This post explores how Certora's security review of 1inch's commit–reveal mechanism helped harden timing windows, deposit infrastructure, and fee configuration — so users can swap across chains with confidence.
The recent theft from the KelpDAO bridge highlights the critical risk of using 1-of-1 security configurations. Moving forward, bridge security requires enforcing multi-DVN quorums and monitoring all infrastructure components to prevent catastrophic single points of failure.
We have released Certora Prover Version 8.11.3 that includes new features.
We provide a roadmap for Stellar smart contract builders to prepare for a security audit through the Soroban Security Audit Bank. By designing for security, writing clean & tool-friendly Rust code, rigorously testing, and running security tools beforehand, projects can be well-prepared. Be audit-ready so your project gets a faster, deeper, and more valuable security review.
"Trustless" bridges claim to allow secure asset exchange across chains even in the presence of malicious actors. However, we argue that truly trustless protocols based on commit-reveal schemes are actually impossible when at least one of the participants does not wait for block finality.
How to design Solidity smart contracts that are easier to formally verify.
Lending protocols may appear simple, but their safety depends on how every operation interacts across the system. In this deep dive, we show how Certora approached the formal verification of Suilend by proving end-to-end properties like solvency, account health consistency, and liquidation profitability.
Together, Aave and Certora demonstrate what is possible when security is treated not as a checkbox but as a core design principle.
The Compound Finance website was manipulated to redirect to a phishing site hosting a lookalike service. Our industry is learning daily that while the on-chain threat persists, the off-chain threat is formidable and growing.
This article explores an observation in the use of BLS signature aggregation within a production blockchain. When it is used for batch verification, the possibility of "conjugate signatures" could allow colluding parties to undermine system properties of accountability and non-repudiation.
This partnership reflects a shared commitment to building a secure, resilient, and developer-first ecosystem, as well as ensuring that Sui-based protocols can scale with confidence as adoption grows.
We explain the vulnerabilities in our first DeFi hacking challenge and announce a relaunch of the contest with a twist: Capture the Funds - Endless CTF!
We have released Certora Prover Version 8.8.0 that includes new features.
Certora has received a research grant from the Ethereum Foundation as part of the zkEVM Formal Verification Project to help secure critical performance optimizations in zkEVM implementations. The work focuses on formally verifying autoprecompiles—automatically generated, reusable ZK circuit components developed by Powdr Labs that significantly improve zkEVM performance.
Last year our security footprint expanded across new chains, languages, and infrastructure layers. Our security research team quadrupled in size. And our work drove home the importance of long-term security partnerships. The numbers here tell that story: not just what we secured in 2025, but the momentum that’s carrying Certora and DeFi as a whole into 2026.
We have released Certora Prover Version 8.6.3 that includes an important enhancement.
Operating a Solana validator under the Solana Foundation Delegation Program requires fast, reliable, and secure infrastructure decisions. Rather than adopting heavyweight monitoring frameworks, we chose a deliberately minimalist approach grounded in Unix principles. This article explains the tradeoffs behind that decision.
Through this initiative, Certora directly contributes to Solana’s decentralization, resilience, and operational security by operating a high-assurance validator built to rigorous security and reliability standards.
We have released Certora Prover Version 8.5.1 that includes new features.
The new Certora AI Composer is an open-source AI coding platform that composes artificial intelligence with formal verification to make smart contract development faster and safer.
On November 3, 2025, Balancer suffered an incident in which attackers manipulated internal vault logic to drain liquidity across multiple blockchains. The breach underscores the importance of prioritizing security even for mature protocols with multiple audits, and it raises urgent questions about composability, operational controls, and the evolving threat-landscape in Web3. Here is Certora’s analysis of the incident, as well as a detailed timeline of events.
The AWS outage and recent security breaches reveal how “decentralized” systems depend on centralized providers. This piece examines how advanced persistent threats could exploit that weakness, and what it means for Ethereum’s trillion-dollar vision.
Concordance is an open-source tool that uses LLMs to automatically rewrite heavily optimized Solidity (including inline assembly) into clear, readable code while preserving all observable on-chain behavior. Each rewrite is proven equivalent by Concord, the equivalence checker, so audits get easier without sacrificing correctness.
Certora presents its first community contests for securing Soroban smart contracts written in Rust. We partnered with Code4rena and Cantina to crowdsource security analysis of the Blend v2 and Aquarius protocols for the Stellar blockchain.
On May 2025, Coinbase faced an incident where attackers gained access to sensitive customer data by targeting support contractors. This article looks at what happened, what it shows about operational security, and how Zero Trust principles can reduce similar risks.
We have released Certora Prover Version 8.1.0 that includes new features and breaking changes.
Our experience formally verifying Rust smart contracts for Soroban and Solana has helped us identify what makes a Rust smart contract easy or difficult to verify. This blog post shares five best practices distilled from our observations to help Web3 developers write Rust smart contracts that are not only secure and readable, but also verifiable.
On July 9th, the Texture team detected that the audited Texture Vaults contract was compromised. Within minutes, the Texture and Certora teams developed and validated a fix via multiple rounds of manual review.
Our engineers identified and corrected a subtle but significant issue in infiniFi's redemption logic through rigorous formal verification, ensuring fairness and trustworthiness. The team ensured that users are treated consistently and predictably under all conditions.
We’ve been working on a compiler equivalence checker named Concord. Given two programs, Concord 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.
