Certora Blog
Technical research and practical perspectives for financial institutions, regulators and builders.
Formal Verification
Formal verification can help DeFi teams catch issues earlier, while AI can make writing and checking specifications more accessible. Drawing on Certora’s work with Aave V4, we explore how developers can use LLMs alongside formal verification, why human judgment remains essential, and how protocols can better protect users when security assumptions fail.
Smart Contract Security
A practical look at Solana program security, from authorization and Token-2022 integrations to oracle checks and accounting invariants, illustrated by findings from Certora audits.
Smart Contract Security
A guide to auditing Daml smart contracts on Canton, from authorization and privacy to contract references, accounting invariants, settlement and topology.
Formal Verification
We examine four ways formally verified systems can fail: incorrect specifications, flawed assumptions, mismatches between verified models and deployed code, and bugs in verification tools themselves. Through real-world examples, we explain how to identify these risks and what to check before relying on a formal verification proof.
Operational Security
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.
Operational Security
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.
Operational Security
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.
Operational Security
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.
Blockchain Infrastructure
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
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.
Operational Security
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.
Product & Company
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.