智能合约审计

:::section{mins=2} What Is an Audit :::

:::lead A smart contract audit is an independent code review by third-party specialists who hunt for vulnerabilities, logic errors, and economic attack vectors before real money is at stake. :::

:::p You're about to deposit money into a DeFi protocol. The website says "Audited by OpenZeppelin" – but what does that actually mean? Who read the code, what exactly did they check, and how much can you trust the result? :::

:::p Auditors read the code line by line, looking for vulnerabilities ([[gloss:reentrancy|reentrancy]], overflow), logic errors in calculations, access control issues (who can call admin functions), and economic attack vectors ([[gloss:flash-loan|flash loans]], [[gloss:oracle|oracle]] manipulation). They deliver a report where each finding is classified by severity – from Critical (total loss of funds) to Informational (code style recommendations). :::

:::p The process: the project locks a specific code version (commit hash), sends it to auditors, who study it for 2–6 weeks, deliver an interim report with findings, the project fixes issues, auditors verify the fixes, and a final report is published. Cost for a major protocol: $50K–$500K+. Top firms have a 3–6 month waiting list. :::

:::p{html} What exactly auditors look for. Those vulnerability classes from above, with a canonical example of each: :::

:::p{html}

:::callout You're buying a house. Before closing, you hire an independent inspector who checks the foundation, wiring, and plumbing. The report comes back: "three serious problems, five minor ones." That doesn't guarantee the house will stand forever, but without the inspection you wouldn't even know the foundation was cracked. A smart contract audit fills the same role: not a guarantee of safety, but the minimum due diligence before trusting code with your money. :::

:::keypoints{label="Key Points"}

• An audit checks a specific commit hash – if the protocol updated its code afterward (and upgradeable proxies allow this without redeployment), the report may be worthless
• Compound lost ~$80M in September 2021 not from a bug in audited code, but from new COMP distribution logic added through a governance proposal after the audit – a textbook illustration of an audit covering only one specific snapshot of the code
• Audit time scales non-linearly: 1,000 LoC takes 1–2 weeks while 10,000 LoC takes 4–8 weeks, because inter-function interactions grow exponentially
• Auditors see the code in the lab – in local simulation, on testnet, in a fuzzer – but they don't observe it in the real economy under the load of real users and real money; behavior in those two environments can diverge (Mango Markets is exactly that kind of divergence) :::

:::details{badge=Advanced title="Inside the Audit Process: From Kick-off to Final Report"} A typical OpenZeppelin or Trail of Bits audit runs in five phases – but each phase catches a different class of bug, and most criticals surface late:

:::p{html}

• Kick-off call (day 1): the team walks auditors through architecture, design intent, and known risk areas. The most underrated phase: without design intent, auditors verify that the code does what it does, not what it should do, which is exactly how economic-design bugs slip through.
• Initial review (days 2-10): each auditor reads the code independently and builds a mental model; scanners (Slither, Mythril) run in parallel. This phase catches the textbook classes (reentrancy, unchecked returns, overflow), roughly the 30-40% an automated tool would flag anyway.
• Deep dive (days 10–25) – cross-functional analysis: how functions interact, what breaks at edge cases, which invariants fail. The majority of true criticals live here, because they're compositions – each function is safe alone. Euler's exploit was exactly this: donateToReserves → distorted health factor → profitable self-liquidation, three safe functions forming one attack.
• Draft report – an interim document with findings by severity. A healthy report on a serious protocol typically contains dozens of findings, mostly low and informational, plus a handful of medium and the occasional high; zero findings across thousands of lines is itself a warning sign – it usually means a shallow review, not clean code.
• Fix review (days 25–35) – the team patches, auditors re-verify. Patches are dangerous: a fix is new, lightly-reviewed code. Euler's $197M line was written in July 2022 to fix a smaller bug, was audited, shipped – and sat live for eight months before it was exploited. The final report records each finding as Resolved, Acknowledged, or Mitigated.

A contest audit compresses initial review brilliantly (hundreds of eyes on textbook bugs) but reproduces the kick-off and deep-dive phases poorly - wardens rarely get design-intent context and are paid to find critical bugs visible in a single function, not the ones that emerge from several functions combined. That's why a contest supplements a traditional audit rather than replacing it. :::

:::further{label="Further Reading"}

• OpenZeppelin – Audit Quality Checklist | blog.openzeppelin.com
• Trail of Bits – Audit Methodology | blog.trailofbits.com :::

:::quiz{id=q-4-2-s1 label="Check yourself" correct=2 explanation="Correct: C. Audit reports classify each finding by severity – Critical (total loss of funds), High, Medium, Low, and Informational (style recommendations). This standardized scale helps teams prioritize fixes."} How does an audit report classify each discovered issue?

• By the auditor's personal preference
• By the time it took to find
• By severity level, from Critical to Informational
• By the programming language used :::

:::section{mins=2} Audit Types :::

:::lead Traditional audits, competitive contests, automated scanners, and formal verification each catch different classes of bugs – and the best strategy combines all four. :::

:::p Say you're launching a lending protocol and want it checked. You have three paths: hire a team of professionals who'll spend a month reading every function; post the code and a prize pool on a contest platform where hundreds of hackers hunt for bugs; or run the code through an automated scanner that catches known vulnerability patterns in minutes. Which to pick depends on your budget, timeline, and protocol complexity. :::

:::p{html} Traditional audit – a team of 2–5 specialists works 2–6 weeks. They work through the architecture, understand the design intent, check every function. What sets it apart from the other types is depth and context: it usually finds the complex logic bugs that automated tools can't and contest wardens skip. It's the most expensive and slowest option (numbers in §9). :::

:::p{html} Competitive audit – the protocol publishes its code and posts a prize pool ($50K–$1M), and hundreds of independent auditors (wardens) hunt for bugs at once. On Code4rena a typical contest draws 30–100 active participants, while Sherlock runs through a curated pool of qualified auditors and adds coverage – insurance against a missed bug. The contest format works best as a supplement to a traditional audit, not as a replacement for it. :::

:::p{html}

:::callout A building has a gas leak hidden somewhere. A traditional audit is hiring one experienced engineer with professional equipment who methodically checks every floor, every pipe joint, and after a week delivers a detailed report. A contest audit is opening the doors and announcing: "Whoever finds the leak gets a prize." Two hundred people show up with varying experience. Collectively they cover more ground in less time. The best strategy: engineer first, then the crowd. :::

:::keypoints{label="Key Points"}

• Code4rena positions itself around finding bugs that traditional audits miss: in 2023 alone, wardens submitted over 3,000 high-severity findings across more than a hundred projects – different approaches catch different bugs, which is why a contest complements a classical audit rather than replacing it
• Contest models have a blind spot: wardens focus on high/critical findings (higher payouts) and systematically skip medium-severity issues that can be critical in combination
• Slither catches ~30–40% of vulnerabilities in minutes for free, but it doesn't understand business logic – it can't know that a lending protocol shouldn't allow borrows exceeding collateral
• The optimal pipeline for a serious protocol: Slither + Aderyn (1 day) → traditional audit (4–8 weeks) → contest (2–4 weeks) → fuzz testing (ongoing) :::

:::details{badge=Advanced title="Auditor Tooling Stack"} An auditor has no single universal tool – they have a stack, and each layer covers a different level of rigor, from a shallow quick scan to a mathematical proof. Knowing what each one catches and where it goes blind matters, because "we ran it through tools" means nothing on its own: the question is which tools, and what they're even capable of seeing.

:::p{html} The first line is static analysis. Slither, from Trail of Bits, parses the Solidity syntax tree (AST – a formal tree representation of the source) and runs it through several dozen built-in detectors: reentrancy, unused return values, variable shadowing. It works in seconds and for free, but it only sees known patterns – its "reentrancy-eth" flag would have caught The DAO before the hack, yet cross-contract dependencies are beyond it. Alongside it sits Mythril from ConsenSys: instead of patterns it builds a mathematical model of every possible execution path, catching overflows and unsafe external calls. The price of that completeness is path explosion – on contracts larger than ~5,000 lines the analysis may never finish in reasonable time. :::

:::p{html} Where static analysis hits its ceiling, fuzzing takes over. Echidna (also Trail of Bits) doesn't hunt for patterns; it runs the contract millions of times with random inputs and checks whether the stated invariants ever break – assertions like "total balance never exceeds supply." This surfaces edge cases a human simply wouldn't think to try: it was Echidna that found a bug in Compound Governor Bravo which two traditional audits had missed. :::

:::p{html} At the top of the rigor ladder is formal verification. Certora Prover doesn't look for bugs – it proves their absence: the team describes a desired property, and the tool mathematically confirms it holds for all inputs and states. MakerDAO, Aave, and Compound rely on it, but the price matches – $100K–$500K on top of a regular audit. For what formal verification can and fundamentally cannot do, see §7. ::: :::

:::further{label="Further Reading"}

• Code4rena – Competitive Audit Platform | code4rena.com
• Slither – Solidity Static Analysis Framework | github.com/crytic :::

:::quiz{id=q-4-2-s2 label="Check yourself" correct=1 explanation="Correct: B. Each layer catches different bug classes. Automated tools find known patterns fast, traditional audits catch logic bugs, contests bring fresh eyes, and fuzz testing runs continuously. No single method covers everything."} What's the optimal verification pipeline for a serious DeFi protocol?

• Contest audit only – many eyes are enough
• Automated scan → traditional audit → contest → fuzz testing
• Traditional audit alone is sufficient
• Slither and Mythril alone – they're free and cover everything :::

:::section{mins=2} Top Auditors :::

:::lead An audit from OpenZeppelin and an audit from an unknown five-person shop are two very different things – the auditor's reputation, tools, and track record matter as much as the audit itself. :::

:::p When you see "Audited" on a protocol's website, the first question is: by whom? Like medicine, a diagnosis from a board-certified specialist and one from a first-year intern are both technically "medical opinions," but they don't warrant the same confidence. Audits are the same – the name of the firm tells you almost more than the fact of the audit itself. :::

:::p That's exactly why serious protocols don't stop at a single audit but go through two, three, or more from different firms – an approach known as multi-audit. Aave v3, for instance, was reviewed by five teams at once (ABDK, OpenZeppelin, PeckShield, Trail of Bits, Sigma Prime) plus formal verification by Certora, and each one caught something the others didn't. It runs $1M and up, but for a protocol with $10B+ in TVL that insurance is more than justified. :::

:::p At the opposite end of the scale are the warning signs. Be wary of an audit from an unknown firm with no public track record, a "rubber stamp" (a report that passed with no findings at all), or a review of an outdated code version. This isn't hypothetical: in 2021–2022 dozens of small shops churned out "clean audits" for $5K–$10K with no serious review, and several of those projects were hacked within weeks of launch. :::

:::p{html}

:::callout When they build a bridge over a river, the design isn't checked by just one engineer – it's reviewed by several, each with a different specialization. One understands load dynamics, another soil composition, a third seismic resilience. None of them covers everything. Multi-audit works the same way: OpenZeppelin excels at finding access control problems, Trail of Bits is strong in cryptographic vulnerabilities, Certora proves correctness formally. A protocol with $10B TVL, like a major bridge, needs all three inspections. :::

:::keypoints{label="Key Points"}

• OpenZeppelin has audited 600+ contracts and maintains the OpenZeppelin Contracts library (used by ~80% of EVM projects) – they know standard patterns better than anyone, but may miss non-standard business logic
• Trail of Bits publishes open-source tools (Slither, Echidna, Manticore) and research – their audits include not just manual review but property-based testing, adding an extra verification layer
• The Aave v3 audit cost ~$1.6M (5 firms + Certora FV), but with TVL >$10B that's 0.016% of protected funds – cheaper than a warehouse lock relative to inventory value
• A practical shortcut: Solodit (solodit.xyz) aggregates findings from across the audit industry into one searchable database. Type in a vulnerability class or a firm name and you see who has caught what – far more useful than trusting any single firm's marketing. :::

:::details{badge=Advanced title="Solo Auditors and Curated Teams"} Individual auditors on Code4rena and Sherlock earn meaningfully less than traditional cybersecurity salaries – but publicly: Code4rena distributed roughly $4.8M across more than 1,300 participants in 2023. The picture flips on Immunefi: per the platform itself, 30 of its researchers have become millionaires, and individual critical findings have paid $1–14M. Names like Trust and pashovkrum carry public track records of hundreds of findings – protocols can judge their effectiveness on concrete metrics rather than firm branding.

Spearbit assembles curated teams per protocol: if auditing a DEX on Solana, they select 3–5 specialists with Solana + AMM experience. Pricing is $150–$300/hour per auditor, roughly comparable to top-tier firms but without the 6-month queue.

A separate model is Sherlock coverage: the protocol pays for an audit, and Sherlock assumes financial responsibility for missed bugs up to a defined limit (typically $1M–$5M). Essentially audit + insurance in one package. :::

:::details{badge=Advanced title="The Firms – and How to Check One Yourself"} First, an honest warning: there is no single objective ranking of audit firms with scores and places. The "top-10 auditors" lists you'll find online are mostly marketing – notice how a firm's own blog tends to rank that same firm at number one. So instead of trusting someone else's leaderboard, it's worth knowing who specializes in what, and learning to check a firm's real track record yourself.

The table below isn't a ranking – it's a map of where the well-known names tend to be strong and where to find their public work. Reputations shift, so treat it as a starting point, not gospel.

:::p{html}

More important than any table is the ability to verify a firm yourself, in a few minutes, before you trust a protocol's "audited" badge:

:::p{html}

• Check the public reports. A serious firm publishes its reports – on its own site, on GitHub, or aggregated on Solodit (solodit.xyz), which collects findings from across the industry in one searchable place. No public reports at all is a red flag.
• Look for relevant experience. A firm strong on EVM lending isn't automatically strong on a Solana AMM or a ZK rollup. Find a past audit of something similar to what you're evaluating.
• Judge the depth, not the page count. Good reports include real Critical/High findings with proof-of-concept exploits, not just style notes. A clean report with zero findings on a large codebase usually means a shallow review, not flawless code.
• Ask what tooling they used. Mentions of fuzzing (Echidna), invariant testing, or formal methods on the risky parts signal a thorough process rather than a manual skim.
• Cross-reference the losses. rekt.news and the DefiLlama hacks tracker list who got exploited and how – useful for sanity-checking a firm's real-world record against its marketing.

:::further{label="Further Reading"}

• OpenZeppelin – Published Audit Reports | openzeppelin.com
• Trail of Bits – Public Research & Publications | github.com/trailofbits
• Solodit – Aggregated Audit Reports & Findings | solodit.xyz :::

:::quiz{id=q-4-2-s3 label="Check yourself" correct=3 explanation="Correct: D. OpenZeppelin excels at access control, Trail of Bits at cryptographic flaws, Certora at formal proofs. Each methodology has blind spots the others can cover."} Why do serious protocols undergo multiple audits from different firms?

• To re-check the same code with fresh eyes – a second pair to catch what the first missed
• Because regulations require multiple audits
• Because audits are cheap enough to stack
• Because different firms catch different types of vulnerabilities :::

:::section{mins=2} Reading an Audit Report :::

:::lead You don't need to understand code to read an audit report. In 10 minutes, answer two questions: did they find serious problems, and were those problems fixed? :::

:::p You've found a protocol, and it has an audit – a 40-page PDF full of technical jargon. The good news is that you don't need to understand the code: to size up the report, four questions are enough. Are all Critical and High findings marked "Resolved," or at least "Acknowledged"? If "Acknowledged" (recognized but not fixed), did the team explain why? Does the audit date match what's deployed right now? And does the scope cover the whole protocol or only a part of it? :::

:::p The reports themselves aren't hard to find: they live in the "Security" or "Docs" section of the protocol's website, in its GitHub repository, on the auditors' own publication pages (OpenZeppelin's, for example), while aggregated security scores sit on DefiSafety.com. :::

:::p A quick read takes about ten minutes. Start with the cover page and scope (a minute) – who reviewed it, when, and which commit hash. Then the executive summary (a couple of minutes) – the tally of findings by severity. Next, the part that matters most: each Critical and High finding (five minutes or so) – what the vulnerability is and what status it carries. And finally the overall picture: a pile of same-type minor errors quietly signals an inexperienced team. :::

:::p{html}

:::callout Ever bought a used car that came with an inspection report? You don't understand engine internals, but you can read: "brake pad wear – fixed," "underbody corrosion – not fixed." That second item is a reason to pause. A DeFi audit report reads the same way: you're looking for the line where "Acknowledged" appears next to a Critical finding – that's your signal that something isn't right. :::

:::keypoints{label="Key Points"}

• "Acknowledged" on a Critical finding isn't always a red flag – sometimes the team consciously accepts the risk (e.g., centralization from an admin key). The real red flag is Acknowledged with no explanation at all
• html: The same Compound incident from KP §1 teaches a separate lesson about response speed: a short governance timelock isn't a bug in itself, but it delays the rollback when something goes wrong. Proposal 062's seven-day timelock prevented a quick halt – and in that window, excess tokens (~$80M) were drained from the contract
• Scope is the main hidden trick: a protocol audits 3 of 7 contracts, then writes "Audited by OpenZeppelin" on its website – technically true, but the 4 unaudited contracts may harbor critical bugs
• A report with zero findings at any level is statistically impossible for >500 LoC: per Trail of Bits, the average audit finds 5–15 issues, of which 0–2 are high/critical :::

:::details{badge=Advanced title="What an Audit Does NOT Cover"} An audit pins the code to a specific commit hash. Everything outside that snapshot stays a blind spot – and attackers aim precisely there.

:::p{html} Upgradeable proxy. Here the blind spot is structural, not accidental: the proxy pattern exists precisely to change code after deployment, while an audit only covers the version it saw. A protocol passes an audit, ships the verified implementation, then a month later swaps in new code via proxy – and that new version was never seen by an auditor. Beanstalk passed an Omniscia audit in April 2022, then added governance logic via upgrade – and that became the entry point. :::

:::p{html} Economic design. The code can be flawless while the logic baked into it is vulnerable. Mango Markets ran exactly per spec, but the spec allowed oracle manipulation: the attacker pumped the price of a collateral token and borrowed against it far beyond its real value. A code audit checks conformance to the spec, not whether the spec itself is sane. :::

:::p{html} Governance attack – the Beanstalk case. This is the clearest example where every individual step is legal. The attacker took a flash loan of roughly $1B (Aave, Uniswap, Sushi), instantly converted it into governance tokens, and gained over two-thirds of the vote. That was enough to push a pre-staged proposal, BIP-18, through the emergencyCommit() function and drain the entire treasury (a second proposal, BIP-19, was a "donation to Ukraine" decoy). It all fit in one transaction: vote, drain ~$182M, repay the loan. A code audit is powerless here – every function ran correctly; the vulnerability was the voting design itself, with no flash-loan resistance. :::

:::p{html} Frontend and infrastructure. Bybit ($1.5B) – the Safe{Wallet} smart contract worked fine, but the frontend was compromised through a supply-chain attack on a developer's machine. An audit doesn't examine the team's CI/CD pipeline or working environment at all. ::: :::

:::further{label="Further Reading"}

• OpenZeppelin – Full Audit Report Archive | openzeppelin.com
• Code4rena – Public Audit Findings | code4rena.com :::

:::quiz{id=q-4-2-s4 label="Check yourself" correct=0 explanation="Correct: A. Critical and High findings represent real threats to user funds. Check whether they're marked “Resolved” (fixed) or “Acknowledged” with a valid explanation. An unresolved Critical without explanation is the biggest red flag."} What's the most important thing to check first in an audit report?

• Whether Critical/High findings are Resolved or have a valid explanation
• The total page count and scope coverage of the audited contracts
• How many Informational and Low findings there are, since they signal audit thoroughness
• The auditing firm's logo and branding, since reputation determines quality :::

:::section{mins=2} Bug Bounties :::

:::lead Bug bounties are continuous crowdsourced security for live code – white hats earn millions finding vulnerabilities in already-deployed contracts, and protocols stay safe between audits. :::

:::p The audit is done, the contract is deployed – what happens next? The code lives on mainnet, and new vulnerabilities can surface at any moment: someone finds an unexpected call combination, an external oracle changes its behavior, a new attack class emerges. The bug bounty is built for exactly this post-audit period – a standing reward for whoever finds a hole and reports it instead of exploiting it. :::

:::p The largest platform here is Immunefi. By the end of 2025 it had paid out more than $120M to white hats, thirty of whom became millionaires in the process; the single largest reward was $10M for a Critical vulnerability in Wormhole. The platform now hosts more than 650 active programs and over 45,000 researchers – so for a serious protocol, the absence of a bounty program is itself a warning sign. :::

:::p It works on the principle of responsible disclosure. A hacker finds a bug and reports it through Immunefi privately, not publicly; the protocol confirms the finding, ships a fix, pays the reward – and only then is the vulnerability disclosed publicly. If instead of disclosing the hacker puts the bug to use, they cross into "black hat" territory and risk criminal prosecution. :::

:::callout You own a jewelry store. You've hired a security firm (the audit), installed cameras and locks. But you know a thief might find a way past all of it. So you post a notice: "Anyone who shows me a way to break in without damage - $10,000 reward." Better to pay $10K for a demonstration of weakness than lose your entire inventory. Bug bounty follows the same logic: protocols pay white hats $1K to $10M for finding holes in their defenses. :::

:::keypoints{label="Key Points"}

• The $10M Wormhole bounty was paid in May 2022 to satya0x for a separate critical bug – an uninitialized upgradeable proxy that could have frozen or drained user funds in the freshly-relaunched bridge. The largest single bounty payout in DeFi history to date.
• Average time from finding submission to payout on Immunefi is 14–45 days; but some protocols delay or dispute validity, creating risk for hackers and reducing disclosure incentives
• Bug bounty sizes vary widely. Aave's current Immunefi program pays up to $1M for a Critical (Aave Labs proposed raising it to $5M, in DAO discussion in early 2026). Wormhole took a different path and set $10M back in 2022 – which is what led to satya0x's record payout. The higher the TVL and risk, the higher the bounty needs to be to outweigh the temptation to exploit.
• A bounty doesn't remove the temptation to exploit, it only shifts the math. Per Hacken's 2025 report, of $4B in losses, $512M (12.8%) came from smart contract vulnerabilities and another $2.12B (53%) from access-control failures: even well-audited code gets attacked through its perimeter, and a low bounty does nothing to stop that. :::

:::details{badge=Advanced title="The Economics of Bug Bounties: What's in It for the Hacker"} Why does someone who has just found a critical bug walk into a chat and ask for a reward instead of quietly draining the contract? Less morality than math: the choice between disclosing and exploiting boils down to expected value, and a bug bounty is an attempt by the protocol to tilt that calculation in its own favor.

:::p{html} The hacker's decision matrix. A researcher has just found a critical vulnerability in a protocol holding $500M of user funds (TVL - total value locked) with a $1M public bounty. Three paths open up. The first is responsible disclosure: report the bug through Immunefi, collect $1M, walk away with zero legal risk. The second is exploit and launder: drain up to $500M and try to wash it through a mixer (a contract that pools and shuffles funds to break the on-chain trail), accepting that Chainalysis and other forensic firms can often follow the money anyway, and that criminal prosecution is a real possibility. The third is the grey-hat path: exploit the bug, then negotiate publicly with the protocol to return most of the money in exchange for a "white-hat fee" – typically 10–15% of the take, plus a great deal of legal ambiguity about whether you've just committed a felony. :::

:::p{html} How real cases mapped onto the matrix. Wormhole's payout to satya0x in May 2022 ($10M, then the largest bounty ever paid) is the clean first path. The irony makes the case: Wormhole had just lost $323M to a different hacker in February, immediately launched a bounty program on Immunefi, and within weeks satya0x quietly reported a separate upgradeable-proxy bug that could have frozen user funds – same protocol, opposite outcome. The bounty program paid for itself many times over before its first quarter was out. Mango Markets ($116M, October 2022) is the second path: Avraham Eisenberg manipulated the protocol's own oracle, called it a "highly profitable trading strategy," and ended up in federal court anyway – convicted in 2024 of fraud and market manipulation. Euler Finance ($197M, March 2023) is the third: the attacker drained the protocol, then over about three weeks negotiated everything back on-chain – no charges were brought, but no formal bounty was earned either. :::

:::p{html} The structural problem with the math. Immunefi's rule of thumb is that an optimal bounty should be roughly 10% of the maximum extractable value – the most a hacker could realistically take. For a $500M-TVL protocol that's $50M, and almost no project can pre-commit such a sum. Real bounty caps therefore sit at 0.1–2% of TVL, often capped at a flat $1M–$10M. The math then flips back in the attacker's favor: on a large protocol, the rational option is no longer disclosure but exploit. What still keeps bounties working in practice is everything outside the spreadsheet – fear of prosecution, the difficulty of cashing out, reputation in the security community, and individual ethics. That gap between the "economically rational" bounty and the one a protocol can actually afford is the soft spot of the industry's post-audit defense, and the part neither audits nor bounties on their own can fix. ::: :::

:::further{label="Further Reading"}

• Immunefi – Web3 Bug Bounty Platform | immunefi.com
• Immunefi – Active Bounty Programs | immunefi.com :::

:::quiz{id=q-4-2-s5 label="Check yourself" correct=2 explanation="Correct: C. Satya0x discovered a repeat critical vulnerability in the Wormhole bridge after its $320M hack and received a $10M bounty – the largest single payout in DeFi bug bounty history as of late 2025."} What was the largest single bug bounty payout as of late 2025?

• $5M to a researcher who reported a critical bug in MakerDAO
• $3M to the Aave bug bounty program
• $10M to satya0x for a Wormhole bridge vulnerability
• $6M from Sherlock coverage for a missed vulnerability :::

:::section{mins=2} Audit ≠ Security Guarantee :::

:::lead Euler Finance passed more than 10 audits and still lost $197M. "Audited" on a website is not a safety guarantee – it's one layer of defense out of seven. :::

:::p Euler Finance passed more than 10 audits – Halborn, Sherlock, Solidified, Certora. It still lost $197M. Ronin Bridge was audited – and lost ~$620M. If that many checks don't save you, why spend money on audits at all? The answer: an audit reduces risk but doesn't eliminate it. :::

:::p{html} Why this is so we've already covered: an audit pins a specific commit hash (see KP §1), its scope doesn't extend to economic design or infrastructure (see advanced §4), and the "audited ≠ safe" thesis itself was introduced in 4.1 §4. Here's the next step: if an audit is just one layer of defense, what other layers complement it, how do they work together, and how do you check yourself whether a given protocol actually has them. :::

:::p{html}

:::p{html} Names in the right column appear elsewhere in the card: Certora and Halmos are covered in detail in §7 (Formal Verification); Forta, OpenZeppelin Defender, and Hypernative – in the user checklist below; Nexus Mutual – there as well, and in 3.5. :::

:::p{html} How a user checks how many layers a protocol actually has. The "audited" badge is easy to verify, but it's only one layer out of seven. The rest leave a public trail too, and most can be seen in five minutes on the project's website. :::

:::howto{label="Five-minute check"}

• Bug bounty. A serious program lives on Immunefi – the project should have its own page (e.g. immunefi.com/bug-bounty/aave) with a stated maximum reward. No page, or language like "a bounty will be launched soon," is a warning sign.
• Monitoring. There's no direct badge, but mentions of Forta, OpenZeppelin Defender, or Hypernative in the Security section or the project's tech blog give it away. Mature protocols mention it openly.
• Circuit breakers. Look in the docs for pairs like pause() / guardian / emergencyShutdown and a description of when they fire. Aave has this logic and documents it; a two-week-old fork usually doesn't.
• Insurance. Check nexusmutual.io: if the protocol is on the list of covered ones, users can buy cover against a hack. That's not a guarantee from the project, but a public signal that underwriters are willing to vouch for it.
• Incident response. Best checked through history: were there past incidents, and how quickly were post-mortems published (24 hours versus two weeks of silence). Mature teams – Yearn, Curve, Compound – usually publish a write-up within a day. :::

:::p{html} The maturity spectrum. Having all seven layers at once is the exception, not the rule. Aave, Uniswap, MakerDAO/Sky really do have close to the full stack: multiple audits, formal verification, an active bug bounty on Immunefi, monitoring, pausers in code, Nexus Mutual coverage, a ready incident-response process. The average DeFi project at launch typically has one or two layers – a single audit and maybe a token bounty. A simple rule: the higher the TVL and the more serious the protocol, the more layers you can see – and the converse holds for a brand-new fork. :::

:::callout You checked all the electrical wiring in your house – everything is fine. But a fire can start from a lightning strike, from a forgotten candle, from the neighbor's house. Checking wiring (code audit) doesn't protect against lightning (zero-day), a candle (operator error – like Ronin), or the neighbor (external oracle dependency). Full fire safety means wiring + lightning rod + smoke detectors + fire extinguisher + insurance + evacuation plan. In DeFi, that's audit + FV + bounty + monitoring + circuit breakers + insurance + incident response. :::

:::keypoints{label="Key Points"}

• Euler: the bug in donateToReserves() altered reserves, which broke the health factor calculation and enabled profitable self-liquidation – each of the three functions passed audit individually, but their combination created the attack vector
• Per rekt.news, as of early 2025 cumulative losses from hacks of projects with at least one audit exceed $5B – audits reduce the probability, but not to zero
• "Audited" without linking to a specific report is a marketing trick – several projects in 2022 claimed "Audited by CertiK" based on a free automated scan, not a full review
• There are no precise public multipliers for how much an audit lowers risk, but the direction is clear: each additional audit by a different firm catches part of what the previous one missed, and the curve of returns flattens quickly. What matters more is that operational and economic risk don't depend on the number of code audits at all – those are covered by different layers of defense. :::

:::details{badge=Advanced title="Zero-day and the Evolution of Attack Classes"} Attack classes don't stand still: almost every year brings a new vector that earlier audits never checked for – simply because it didn't yet exist. The history of DeFi hacks is the history of defense forever catching up to offense.

In 2016–2019, basic code bugs ruled: reentrancy (The DAO, $60M) and integer overflow (batchOverflow, 2018). Auditors learned to catch these, and by 2020 they had all but vanished from audited contracts. But a new front opened immediately: in February 2020 the bZx attack ($350K) became the first in history to use flash loans – before it, no audit had even considered the vector, because the instrument itself didn't previously exist.

In 2021–2022 the center of gravity shifted to bridges and governance: Ronin ($620M), Wormhole ($320M), and Nomad ($190M) made cross-chain bridges the single largest category of losses, while Beanstalk ($182M) showed how a flash loan could hijack the vote itself. By 2024–2025 the attack had moved even further from the code, into infrastructure: Bybit ($1.5B) was breached through a compromised developer machine, and Ledger Connect Kit through a tampered npm package.

An audit reliably covers the "known knowns" - what we already know how to look for. Monitoring (Forta, Hypernative) picks up the "known unknowns," tracking anomalies in real time. But the "unknown unknowns" - a fundamentally new class no one has seen yet - are covered by nothing except insurance and a pre-planned incident response. :::

:::further{label="Further Reading"}

• DeFiSafety – Protocol Security Ratings | defisafety.com
• Forta Network – Real-time Threat Detection | forta.network :::

:::quiz{id=q-4-2-s6 label="Check yourself" correct=1 explanation="Correct: B. The donate function, health factor calculation, and liquidation logic each passed audits. But donating to reserves altered the health factor in a way that enabled profitable self-liquidation – a composition bug that individual function reviews couldn't catch."} Why did Euler Finance lose $197M despite more than 10 audits?

• The vulnerable code was added after all the audits were done
• Each function was safe individually, but their combination created an exploit
• The audits were fake rubber stamps
• Ten audits weren't enough – twelve would have caught the bug :::

:::section{mins=2} Formal Verification :::

:::lead Formal verification proves mathematically that code matches its specification for all possible inputs – not "we didn't find a bug," but "this class of bug is impossible." :::

:::p An auditor can miss a bug – they're human. Is it possible to check code so that the guarantee is mathematical rather than expert-based? It is – but it costs a lot and only covers what you explicitly describe in a specification. :::

:::p Here's how formal verification works: you describe in a formal language exactly what the code should do (for example, "after calling withdraw(amount), the user's balance decreases by exactly amount"). A tool checks this statement for all possible inputs and all contract states. If the proof passes – [[gloss:reentrancy|reentrancy]] in that function is mathematically impossible. :::

:::p The main FV tool in DeFi is Certora (which we've already met in §2). Around it are property-based fuzzers and narrower academic systems – each with its own place in the stack: :::

:::p{html}

:::p{html} A quick word on the lesser-known names. Halmos (by a16z crypto) is an open-source symbolic checker for Solidity – same idea as Certora but free and lighter, suited to teams that can't justify a full Certora budget. K Framework is the academic pole: it formalizes the entire EVM at the bytecode level and was used to write the formal specification of the EVM itself. SMTChecker is built into the Solidity compiler – basic, doesn't require setup, but only catches a narrow class of properties. :::

:::callout In chess, an auditor is a grandmaster who looks at a position and says: "I don't see a way to checkmate." He can be wrong - his attention and time are limited. Formal verification is a program that brute-forces every possible move sequence to the end of the game and proves: "Checkmate is impossible in any sequence of moves." A mathematical guarantee, but only for the rules you described. If you didn't account for the opponent flipping the board, the program won't check for that either. :::

:::keypoints{label="Key Points"}

• Certora proved for MakerDAO that under no conditions can DAI supply exceed the debt ceiling – this isn't "we checked and didn't find a bug," it's "mathematically impossible" across all 2^256 possible states
• Aave v3 used Certora to prove a solvency invariant: total deposits ≥ total borrows – this property was verified for every combination of market operations
• Real-world limitation: Certora would not have caught the Euler bug, because donateToReserves() didn't formally violate any recorded invariant – the problem was an unexpected interaction nobody described in the specification
• Fuzz testing (Echidna, Foundry) is FV's budget version: instead of checking ALL paths it runs millions of random ones, catching ~80% of what FV would, but at 10–50x lower cost :::

:::details{badge=Advanced title="FV Limitations: What Math Doesn't Cover"} Formal verification looks like a silver bullet: a proof either passes or it doesn't, with no room for human error. But its strength is also where its limits live. Three of them are systemic – they don't go away with a better tool – and the third forces a practical compromise that the best teams now treat as standard.

:::p{html} The incomplete-specification problem. FV proves that the code matches its specification – but humans write the specification, and humans miss properties that feel "obvious." Picture a real case: Certora proved for a lending protocol that a user's balance can never go negative and that the total token supply is constant. Both proofs passed. But nobody wrote a rule saying "a user must not be able to withdraw funds they've already pledged as collateral in another market" – that property simply didn't make it onto the list. And that was exactly the gap an attacker exploited. The proof was correct; the specification was incomplete. The more complex the system, the more "obvious" rules a team forgets to articulate, and an FV tool can only verify the rules it's given. :::

:::p{html} Cross-contract interactions. Even within one contract, a thorough specification is hard. DeFi makes it harder still, because protocols are composable building blocks: a single user transaction can take a flash loan on Aave, swap on Uniswap, deposit the result into Compound, and unwind everything before the block closes. Each protocol was verified separately; the combination was verified by no one. And in principle, it can't easily be: every new contract in the chain multiplies the state space the prover has to search, and the problem quickly becomes NP-hard – a class of problems where the time needed grows so fast that no machine can finish in a reasonable timeframe. Certora doesn't solve full multi-protocol composition, and neither does any other production prover today. :::

:::p{html} The practical compromise: fuzzing as the working alternative. A full Certora verification of an entire protocol costs $100K–$500K and takes weeks of specification writing. Doing it for every contract is unaffordable for almost anyone. Trail of Bits – who themselves build fuzzing tools – publicly recommend a hybrid: invariant testing with Echidna or Foundry's fuzzer ($5K–$20K) across the entire codebase, and full Certora-style FV only on the parts where money actually moves, the withdrawal and liquidation paths ($100K–$500K). Fuzzing doesn't prove the absence of bugs the way FV does, but on a multi-million-transaction run it finds violations of stated invariants quickly and across the whole system. The combination buys ~95%+ practical coverage at roughly three to five times less than a full FV of every line – and that's the recipe most security-mature teams quietly settle on once they hit the cost wall. :::

:::p{html} K Framework – the academic pole. The only tool capable of verifying EVM semantics at the bytecode level rather than at Solidity level. The EVM specification itself was formalized in it. Academically powerful, but the complexity and cost of writing specifications make it impractical for everyday audits. ::: :::

:::further{label="Further Reading"}

• Certora – Formal Verification Platform | certora.com
• Echidna – Property-based Fuzz Testing | github.com/crytic :::

:::quiz{id=q-4-2-s7 label="Check yourself" correct=3 explanation="Correct: D. FV proves that code conforms to its specification for ALL possible states and inputs – a mathematical guarantee. But it only covers what the specification describes. If a property isn't in the spec, FV doesn't check for it."} What does formal verification prove about smart contract code?

• That the code has no bugs at all
• That every line was reviewed by auditors
• That the code will remain secure after future upgrades
• That the code matches its specification for all possible inputs :::

:::section{mins=2} Anatomy of Major Hacks :::

:::lead The largest crypto hack in history – Bybit's $1.5B loss in February 2025 – happened not because of a smart contract bug but because a developer's machine was compromised. Real cases show where audit coverage ends. :::

:::p{html} If audits regularly miss bugs even after ten reviews, what kind of bugs are these? The category that has hurt audited protocols most is the composition bug – a vulnerability where every individual function is correct, the spec is followed, and yet a specific chain of those safe functions, in the right order, breaks the whole system. This is the bug class that explains why even multi-million-dollar audit programs aren't enough on their own. :::

:::p{html} The clearest specimen is Euler Finance, March 2023. The protocol's donateToReserves let a user voluntarily give assets to the protocol's reserves – useful, harmless on its own. The health-factor calculation determined whether a position was safe to keep open – standard, correct math. The liquidation function let undercollateralized positions be closed – exactly what a lending protocol must do. Each function passed audit individually, in ten separate reviews. But together they composed an attack: donate to distort the reserves, push your own health factor into the "must liquidate" zone, then liquidate yourself – and because the math now lied about the position's true state, the liquidation paid out more than you put in. $197M, gone in seconds. :::

:::p{html} Composition bugs aren't the only way audited protocols fall. They share the field with three other categories, each already covered earlier in the card: key-management failures (Ronin, $620M – the multisig itself was sound; five of nine keys ended up at one company), economic-design exploits (Mango Markets, $116M – the code did exactly what the spec said; the spec allowed oracle manipulation, see §5), and operational compromise (Bybit, $1.5B – a developer's machine, never in any audit's scope, see §4). The four together describe almost every nine-figure loss of the last three years. :::

:::callout Every engine, every system in an airplane is certified separately, and each works flawlessly. But in 1988, Aloha Airlines Flight 243 lost part of its fuselage not because any single system failed, but because of a combination of factors: metal fatigue + salt air + thousands of pressure cycles. Each factor individually passed inspection. Their combination didn't. Euler Finance lost $197M by the same logic: donate and health factor check passed audit separately, but their combination created the exploit. :::

:::keypoints{label="Key Points"}

• Per rekt.news, of the top-10 largest hacks by 2025, 6 happened to audited projects – but in 4 of those 6, the root cause wasn't code but key management or economic design
• Euler returned funds through on-chain negotiations in about three weeks; Ronin compensated users with Binance's help over several months; but Nomad ($190M, 2022) returned almost nothing – fund recovery is not guaranteed
• Cetus on Sui ($223M, May 2025) – an integer overflow in concentrated liquidity math was found about a month after the audit; the bug was in a math library outside the audit scope
• 2024–2025 trend: operational attacks (supply-chain, social engineering) bypass any code audit – Bybit ($1.5B) and Ledger Connect Kit ($600K) were hacked through dev infrastructure, not smart contracts :::

:::details{badge=Advanced title="After the Hack: Who Got Their Money Back – and Who Didn't"} Once an exploit happens, the statistics favor the attacker: per De.Fi, in 2022 only about 2% of stolen funds were recovered on average; in 2023 the figure climbed to around 10%. Those averages hide enormous variance. If the right conditions line up for a particular protocol, recovery can be near-complete; if they don't, users are out of pocket. The outcome depends on which of four recovery mechanisms is actually available.

:::p{html} Mechanism one: negotiation with the attacker. The best-known case is Euler Finance ($197M, March 2023). Instead of going straight to law enforcement, the team posted an on-chain message – "return the funds, keep a bug bounty" – and spent roughly three weeks bargaining with the attacker publicly through the blockchain. In the end the attacker returned everything, and because ETH appreciated during the talks, the protocol got back even more than was stolen, around $240M. This mechanism works when the attacker hasn't yet moved funds to an exchange and realizes they're legally cornered. It triggers rarely: you need a willing-to-talk attacker, a prepared team, and a protocol able to raise enough "white noise" around its incident. :::

:::p{html} Mechanism two: bailout from a related entity. Wormhole ($320M, February 2022) returned nothing to users itself – and didn't have to: the very next day Jump Crypto, Wormhole's parent fund, replaced 120,000 ETH out of its own capital. This is a "parental guarantee" in the TradFi sense: users were made whole not by the protocol but by the VC firm behind it. A similar but far slower scenario played out at Ronin (~$620M, March 2022): Sky Mavis raised $150M led by Binance and added its own funds; compensation stretched over months, and 56,000 ETH from the Axie DAO treasury stayed undercollateralized. This mechanism saves users but not the protocol – it shows the security depended on the solvency of a "sponsor of last resort," not on the code. :::

:::p{html} Mechanism three: counter-exploit. The rarest and most revealing case for the industry came in February 2023, a year after the Wormhole hack. Jump Crypto, in partnership with the team behind the Oasis multisig wallet, found a technical hole in the attacker's own wallet and counter-exploited 120,000 ETH (about $140M) back. Legally and ethically it lives in a gray zone: exploiting a flaw in someone else's wallet, even a hacker's, doesn't fit the simple "victim recovering their own" frame. But as a proof of concept it matters: technically pulling funds back is possible if the attacker has a connected wallet with a weak spot. :::

:::p{html} Mechanism four: criminal prosecution without recovery. Mango Markets ($116M, October 2022) – Avraham Eisenberg called his actions a "highly profitable trading strategy," boasted about them publicly, and in 2024 was convicted in the US of fraud and market manipulation. He never voluntarily returned the funds. For users this is the worst outcome: justice happened, the money didn't come back. Much the same with Nomad ($190M, August 2022): the exploit was so trivial that hundreds of random addresses piled in, only about $32M was voluntarily returned to the recovery wallet, and prosecution of most participants went nowhere. The fresh Bybit case ($1.5B, February 2025) shows this mechanism's ceiling: per TRM Labs estimates, by early 2026 less than 5% had been recovered – the bulk of the funds, traced to Lazarus Group, had already dissolved into a distributed laundering infrastructure: the bulk of the ETH was routed through THORChain and cross-chain bridges and converted into BTC (per Bybit itself, about 86% by late March 2025), from there scattered across Bitcoin mixers (Wasabi, CryptoMixer, Railgun) and no-KYC P2P vendors. TRM Labs notes that underground financial networks linked to China play a substantial role in absorbing these funds. Against that backdrop, any future convictions will barely change the outcome. :::

:::p{html} What this means for users. Your odds of getting money back are set not by the audit but by which of these four mechanisms is actually available to a given protocol. Negotiation – if the attacker was after a bounty, not the money. Bailout – if there's a solvent sponsor willing to plug the hole. Counter-exploit – almost never. Justice – slow, and usually without recovery. Real protection comes not from the "audited" label but from a pre-planned incident response and a reserve fund: those two layers in the §6 table are exactly the preparation for running one of these four mechanisms in real time. ::: :::

:::further{label="Further Reading"}

• Rekt.news – Hack Leaderboard | rekt.news
• Chainalysis – Crypto Crime Report | chainalysis.com :::

:::quiz{id=q-4-2-s8 label="Check yourself" correct=0 explanation="Correct: A. Bybit ($1.5B) was hacked through a compromised dev machine, Ronin ($620M) through stolen keys, Multichain ($126M) through a CEO's personal server. By 2025, the largest losses come from operational failures, not code bugs that audits can catch."} What's the dominant trend in crypto hacks by 2025?

• Operational security failures (key compromise, supply-chain) now cause larger losses than code bugs
• Reentrancy remains the dominant attack vector, despite improvements in audit tooling and coding standards
• Cross-chain bridges remain by far the most-attacked category
• Flash-loan attacks have grown by an order of magnitude and dominate the threat landscape by total loss volume as of 2025 :::

:::section{mins=2} Audit Economics :::

:::lead Euler Finance spent over $1M on 10+ audits and still lost $197M – but without those audits, it would likely have lost everything much sooner. The question isn't whether to audit, but how much to spend for your scale. :::

:::p The price of an audit comes down to several factors, and the biggest is the volume of code: top firms charge roughly $10–50 per line. From there it depends on the complexity of the logic (DeFi lending is harder to dissect than a simple token, which is harder than an NFT), on the firm's tier (OpenZeppelin charges three to five times more than an unknown shop), and on urgency (jumping the queue adds a 50–100% rush fee). Anything beyond the EVM costs extra on its own: an audit on Solana/Rust or Move runs two to three times more – fewer specialists, almost no ready-made tooling. :::

:::p Against the sums being protected, even those figures look modest. According to Token Terminal, MakerDAO (now Sky) spends about $3.9M a year on security on roughly $5.8B in TVL (as of early 2026) – less than 0.07% per year, whereas a bank spends 5–10% of revenue on compliance. For a DeFi protocol, auditing is one of the cheapest forms of insurance there is. :::

:::p The flip side follows from this: an expensive audit isn't always necessary. A project with under $100K of expected TVL, an unmodified fork, or a throwaway contract can get by with an automated scan and a single solo auditor. Multi-audit, by contrast, becomes mandatory wherever the cost of a mistake is highest – for bridges (cross-chain is the highest risk), protocols with TVL above $100M, contracts upgradeable via proxy, and genuinely novel mechanisms with no battle-tested precedent. :::

:::p{html} Cost factors at a glance. The same factors laid out above, condensed into a quick-reference table – handy when you're sizing up a quote and want to check what's driving the number. :::

:::p{html}

:::callout Ever wonder how much an airline spends on aircraft maintenance? About 10–15% of operating costs – tens of millions of dollars per aircraft per year. Nobody calls that "expensive," because the alternative is a crash. MakerDAO spends ~$3.9M/year on security with ~$5.8B TVL – less than 0.07% per year. Banks spend 5–10% of revenue on compliance. For a DeFi protocol, auditing is one of the cheapest forms of insurance. :::

:::keypoints{label="Key Points"}

• Non-EVM audits (Solana/Rust, Move/Sui, Cairo/Starknet) cost 2–3x more than EVM – there are fewer Rust security specialists than Solidity experts, and tools like Slither don't exist for Rust
• MakerDAO spends ~$3.9M/year on security with ~$5.8B TVL (0.07%) – by comparison, a bank spends 5–10% of revenue on compliance; DeFi security costs are anomalously low relative to protected sums
• Uniswap v4 went through nine independent audits before launch – OpenZeppelin, Trail of Bits, Certora, Spearbit, ABDK, and Pashov Audit Group – plus a public security competition with a $2.35M prize pool and 500+ researchers. After all that, a $15.5M bug bounty was opened on top, the largest in DeFi history. For a protocol with billions in TVL, this isn't overkill – it's the floor. :::

:::details{badge=Advanced title="Audit Market Dynamics and New Models"} The audit market behaves like a market in its own right – with queues and prices that track the mood of crypto. During a bull market, top firms are overloaded: projects rush to launch at once, queues at OpenZeppelin or Trail of Bits can stretch into months, and prices climb on hot demand. In a bear market the picture flips – queues shrink, terms soften, and mature teams like Aave and Uniswap use those lulls to review upcoming versions calmly.

The working model is shifting too. A one-off audit fits poorly with protocols that ship updates constantly, so a continuous-audit subscription emerged: through OpenZeppelin Defender plus a retainer, a protocol pays $20K–$50K a month and every significant commit gets reviewed. The arithmetic comes out comparable to a one-off audit – ten updates a year at $30K is the same ~$300K – but it covers the whole year rather than a single snapshot of the code.

Finally, in 2024–2025 AI has clearly entered the process. Olympix plugs into the CI/CD pipeline and runs automated checks on every commit; Code4rena's own 4naly3er handles routine gas-inefficiency detection; LLM-based tools are starting to reason about business logic. This compresses the initial scan, but it doesn't replace manual review: for genuinely novel mechanisms there's nothing for a model to learn from. Mature teams already treat AI as a triage accelerator, not an auditor replacement. :::

:::further{label="Further Reading"}

• OpenZeppelin Defender – Security Monitoring | openzeppelin.com
• Cyfrin Updraft – Free Security Course | updraft.cyfrin.io :::

:::quiz{id=q-4-2-s9 label="Check yourself" correct=2 explanation="Correct: C. MakerDAO (now Sky) spends ~$3.9M/year on security with ~$5.8B TVL – just 0.07%. By comparison, traditional banks spend 5–10% of revenue on compliance. DeFi security costs remain anomalously low relative to the value they protect."} What percentage of TVL does MakerDAO spend on security annually?

• About 5%
• About 1%
• About 0.07%
• About 10% :::