Week 15 — Audit Methodology & Tooling

“A junior auditor stares at the diff. A mid-level auditor reads the code top-down. A senior auditor reads the docs first, asks ‘what is this trying to protect?’, writes down five invariants, and only then opens a file. The methodology is what separates a bug-hunter from a security engineer — and clients pay for the engineer.”

Tags: web3-security methodology tooling slither echidna medusa foundry halmos certora severity Learner: Has completed Weeks 1–14; needs to convert technical skill into professional audit output Time: 7 days (6–7h/day; the densest professional-practice week) Related: Tuan-04-Security-Foundations-CEI-AC · Tuan-05-Vulnerability-Classes-Part-1 · Tuan-06-Vulnerability-Classes-Part-2 · Tuan-09-Oracle-MEV-Economic-Attack · Tuan-16-Report-Writing-Capstone

1. Context & Why

1.1 What this week is and isn’t

It is not: “here are some tools, learn the flags.”

It is: the production process by which a security engineer takes an unknown codebase and produces a deliverable a sophisticated client will accept. The tools are a means; the methodology is the work.

By Friday you should be able to:

Scope an unknown protocol (in-scope contracts, trust assumptions, complexity estimate, day-count estimate, deliverables).
Threat-model it (per-actor; STRIDE adapted to Web3; trust boundaries on a diagram).
Identify invariants at the protocol-wide and per-module level.
Run a layered tool sweep: Slither → custom detectors → Echidna/Medusa fuzzing → Foundry invariant tests with handlers → Halmos symbolic checks → (optional) Certora rules.
Conduct manual review top-down, bottom-up, and cross-cutting; keep a running finding journal that becomes the report.
Classify severity under the Immunefi / Code4rena / Sherlock conventions and defend the call to a client who disagrees.
Plan remediation review: not “did they fix it” but “did the fix introduce something new”.

If you can do these seven things on a protocol you’ve never seen, you can be paid for audits. If you can’t, you’re a bug-hunter — which has a place, but the ceiling is lower and the work less reliable.

1.2 The mindset shift

The shift from Week 14 to Week 15 is the shift from finding bugs to delivering a service.

A bug-hunter optimises for one big finding. An auditor optimises for coverage + signal: every external entry point reviewed, every storage slot mapped, every reasonable bug class checked, with a written record.
A bug-hunter writes a PoC. An auditor writes a PoC plus a description, an impact analysis, a severity rationale, a recommended fix, and re-verifies the fix.
A bug-hunter works alone. An auditor works in a methodology that’s reproducible by another auditor so the client gets a consistent result regardless of who’s on the engagement.

Treat this as engineering, not art. The art shows up in the bugs; the engineering shows up in the report quality, the consistent severity calls, the survived push-back from the client, and the lack of escapes (bugs the audit missed that show up post-launch).

1.3 Learning goals

By the end you can:

Produce a one-page scoping document for an unknown protocol within 30 minutes of reading.
Build a threat model document with explicit actors, trust boundaries, and a STRIDE-derived risk table per component.
Write an invariant list for an AMM, a lending market, and an ERC-4626 vault from memory.
Run Slither, Echidna, Medusa, Halmos in a single repo and explain why each found (or missed) a given bug.
Write a custom Slither detector for a project-specific anti-pattern.
Defend a Medium severity call against client pressure to downgrade to Low — citing the Immunefi or Sherlock rubric verbatim.

1.4 Primary references

Source	URL	Status
Trail of Bits — Building Secure Contracts	https://github.com/crytic/building-secure-contracts	Current — the canonical methodology reference; Slither/Echidna/Medusa-centric
Slither	https://github.com/crytic/slither	Current (v0.11.5 as of Jan 2026 — [verify])
Echidna	https://github.com/crytic/echidna	Current (v2.3.2 — [verify])
Medusa	https://github.com/crytic/medusa	Current (v1.5.1 — [verify])
Foundry Invariant Testing	https://getfoundry.sh/forge/invariant-testing	Current
Halmos	https://github.com/a16z/halmos	Current (v0.3.x — [verify])
Certora Prover Docs	https://docs.certora.com/	Current — CVL spec language
Tenderly	https://tenderly.co/	Current — simulator + monitoring
Aderyn (Cyfrin)	https://github.com/Cyfrin/aderyn	Current — Rust-based static analyzer, ~100 detectors [verify]
Immunefi Severity Classification v2.3	https://immunefi.com/immunefi-vulnerability-severity-classification-system-v2-3/	Current
Sherlock Judging Guidelines	https://docs.sherlock.xyz/audits/judging/guidelines	Current — high/medium-only platform, strict rubric
Code4rena Severity Rubric	https://docs.code4rena.com/competitions/submission-guidelines	Current
OWASP Smart Contract Top 10 (2025)	https://scs.owasp.org/sctop10/archive/2025/Top10:2025/	Current — useful as a checklist floor, not a method
SWC Registry	https://swcregistry.io/	Partial — historical reference; many entries still valid but not actively updated
ConsenSys Diligence — Smart Contract Best Practices	https://consensys.github.io/smart-contract-best-practices/	Partial — reentrancy / CEI material current; randomness section outdated (use VRF)
Spearbit / Cantina methodology	https://cantina.xyz/blog/security-review-readiness-guide	Current — protocol-side readiness expectations

2. The Audit Lifecycle

2.1 The full pipeline

flowchart TD
    A[Pre-engagement<br>Scoping · NDA · Quote] --> B[Kickoff<br>Walkthrough · Docs · Threat assumptions]
    B --> C[Threat Modeling<br>Actors · Boundaries · STRIDE]
    C --> D[Invariant Identification<br>Per-module · Protocol-wide]
    D --> E[Static Analysis<br>Slither · Aderyn · Custom detectors]
    E --> F[Manual Review<br>Top-down · Bottom-up · Cross-cutting]
    F --> G[Fuzzing<br>Echidna · Medusa · Foundry invariant]
    F --> H[Symbolic / Formal<br>Halmos · Certora · K]
    G --> I[Findings Consolidation<br>Dedupe · Severity · Sanity]
    H --> I
    I --> J[Report Draft<br>Week 16]
    J --> K[Client Q&A<br>Defend severity · Adjust]
    K --> L[Remediation Review<br>Re-audit fixes · Confirm no regressions]
    L --> M[Final Report]
    style C fill:#fff2cc
    style D fill:#fff2cc
    style F fill:#ffd6a5
    style I fill:#caffbf
    style L fill:#a0c4ff

Each stage has a deliverable. If you don’t produce the deliverable, you didn’t do the stage.

Stage	Time share	Deliverable
Pre-engagement	5%	Scoping doc, signed engagement letter
Kickoff	5%	Notes on docs / assumptions / open questions
Threat modeling	10%	Threat model document with diagram
Invariant identification	5%	Invariant list (per module + global)
Static analysis	5%	Slither/Aderyn report, triaged
Manual review	40%	Running findings journal
Fuzzing	15%	Fuzz harness + corpus + any failing properties
Symbolic/formal	5%	Halmos/Certora rules (optional per engagement)
Findings consolidation	5%	Deduplicated, severity-assigned finding list
Report draft + Q&A	5%	Polished report (Week 16)
Remediation review	5%	Remediation report

The %‘s assume a fixed-scope private audit. Competitive contests (C4/Sherlock/Cantina) skew differently — almost all time on manual + fuzz, no scoping/quote/remediation, judging handles severity.

2.2 Time-box discipline

Audit work expands to fill available time. Without a clock, you re-read the same function five times and never look at the second contract. Practical structure for a 10-day engagement:

Day 1   : Scope, kickoff, docs read-through, threat model v0
Day 2   : Threat model finalize, invariant list, Slither/Aderyn first pass
Day 3-4 : Top-down manual review (entry points → state changes)
Day 5-6 : Bottom-up manual review (storage variables → who writes them)
Day 7   : Cross-cutting passes (access control, events, modifiers, math)
Day 8   : Fuzzing harness (Echidna / Foundry invariant) + run overnight
Day 9   : Symbolic/Halmos rules on hotspots; consolidate findings
Day 10  : Severity calibration; report draft skeleton

After kickoff, never go a full day without writing in the finding journal — even “no findings, reviewed X.sol” is a journal entry. The journal is your honesty mechanism.

3. Pre-engagement & Scoping

3.1 What goes into a scoping document

A scoping doc is a one-page contract-on-the-contract. Headers:

Repo + commit hash (frozen) — audits are against a specific git SHA, not a moving target.
In-scope contracts — explicit list. Include file paths and approximate SLOC.
Out-of-scope — explicit list. Front-end, off-chain keepers, deployment scripts unless requested.
Trusted assumed-external dependencies — OZ contracts (specific versions), Chainlink feeds, Uniswap V2/V3, Curve. Spell them out — “trusted” doesn’t mean “ignored”; it means “we accept their published behavior as ground truth”.
Trust assumptions — who can do what? Owner, governance, multisig, keeper, anyone.
Threat models the client cares about — “we worry about MEV”, “we worry about flash-loan governance”, etc.
Out-of-scope threats — “L1 reorg”, “compiler bugs”. State these so they’re not surprises later.
Day estimate — see §3.3.
Deliverables — threat model doc, invariant list, draft report, final report, remediation report.
Timeline & milestones — kickoff date, draft due, remediation review window.

The scoping doc is your shield against the eternal “but you should have caught X” — if X is the front-end and the scope said contracts only, you point at the scope.

3.2 SLOC, complexity, and “audit day” estimation

Industry rule of thumb for manual review pace:

Codebase type	SLOC reviewed per auditor-day
New code, no docs, novel design	100–300
Standard DeFi, documented, OZ-based	300–800
Re-audit / incremental review	500–1500
Heavily-tested, well-known fork (e.g., Uniswap V2 fork)	1000–2000

Don’t promise more than this without good reason. A “1000 SLOC AMM audit in 2 days” pitch is a red flag — for the client or the auditor.

Multiply for complexity:

× 1.5 if upgradeable proxies (storage layout work).
× 1.5 if novel math (curve fitting, custom AMM invariants, bonding curves).
× 1.5 if cross-chain message passing.
× 1.5 if integrates with multiple unfamiliar external protocols.
× 2 if assembly / Yul / inline opcodes.

For a 2000-SLOC vanilla ERC-4626 fork at 500 SLOC/day: 4 auditor-days minimum, 6 with cushion. For 2000 SLOC of novel bridge code: 4 × 2 (cross-chain) × 1.5 (novel) = 12 auditor-days.

Add scoping + reporting + remediation at ~30% on top.

3.3 Day rate & fees (orientation, not advice)

Rates vary widely. Typical 2026 ranges for solo / boutique auditors:

Tier	Range (USD/day)
New independent auditor (1st-year, portfolio building)	$500-$ 1,000
Established independent	$1, 500-$ 3,000
Spearbit / Cantina lead-tier solo researcher	$3, 000-$ 5,000+
Top-firm engagement (multi-auditor, multi-week)	$2, 500-$ 5,000/auditor/day

Quote in auditor-days, not flat fees, when the scope is uncertain. The client knows their codebase grew last week.

3.4 NDA, COI, disclosure norms

NDA: standard for private audits. Limits public discussion of findings until disclosure.
Conflict of interest: disclose token positions, prior engagements with the client, or relationships with the client’s competitors. The default is “decline if material exposure”.
Disclosure: most clients want findings public after remediation + a cooling-off window. Some keep them private indefinitely (rare, sketchy).
Bug found during audit that’s exploitable on mainnet: stop. Coordinate immediate disclosure to the client; if no response within a few hours, escalate via Immunefi.

3.5 Scoping deliverable template

# Scoping — <Project> Smart Contract Audit
**Audit period**: <start> → <end>
**Auditors**: <name(s)>
**Commit hash**: <sha>
**Compiler**: <solc version>
 
## In Scope
| Contract | Path | SLOC | Complexity |
|----------|------|------|-----------|
| Vault.sol | src/Vault.sol | 412 | High (custom math) |
| Router.sol | src/Router.sol | 280 | Medium |
| ...
 
Total: ~1,400 SLOC, est. 5 auditor-days manual + 2 days tooling + 1 day report = 8 auditor-days.
 
## Out of Scope
- frontend/* (not requested)
- deploy/* (deployment scripts)
- third-party libraries (@openzeppelin/contracts v5.0.2 — assumed trusted)
- Chainlink price feed integrity (assumed trusted within Chainlink's published model)
 
## Trust Assumptions
- `owner` role: protocol multisig, 3-of-5, governance-controlled.
- `keeper` role: off-chain bot, assumed honest but liveness not guaranteed.
- Chainlink ETH/USD feed: assumed correct within 0.5% over 1-hour windows.
 
## Threats Examined
- All OWASP SC Top 10 2025 categories.
- Read-only reentrancy on Vault.virtualPrice().
- Donation attack on ERC-4626 share accounting.
- Flash-loan-driven oracle manipulation against Router.
 
## Out of Threat Scope
- Compiler bugs (assumed solc 0.8.24 correct).
- L1 reorg deeper than `finalized` tag.
- Cross-chain messaging (no bridge in this audit).
 
## Deliverables
1. Threat model document (Day 2)
2. Invariant list (Day 3)
3. Draft report (Day 8)
4. Final report (Day 10)
5. Remediation review (within 5 business days of fix delivery)

4. Kickoff & Documentation Review

4.1 Documentation as evidence

Before reading code, read everything else:

Source	What you’re looking for
README	High-level intent, “what is this” in plain English
Whitepaper / litepaper	Economic model, incentive structure, intended invariants
Spec / NatSpec	Per-function preconditions and postconditions
Test suite	What the developers think must hold (their assumed invariants)
Deployment scripts	Init order, parameter values, role assignments — most ignored, often most revealing
Prior audit reports	Known issues, prior remediation patterns — a floor, not a ceiling

Auditor instinct: when docs and code disagree, you have a finding. Either the code is wrong (a bug) or the docs are wrong (a doc bug — still a finding, because users base decisions on docs).

4.2 The “first 60 minutes” walkthrough

Spend the first hour of kickoff on a developer-led walkthrough:

“Walk us through the happy path — a user does X, what contracts touch their state?”
“What’s the worst thing an attacker could do?”
“What kept you up at night during development?”
“Where did you cut corners?”
“What changed since the last audit?”

Developers tell you the bugs if you ask. They know the cliffs. Their answers go straight into the threat model.

4.3 Setting up your repo

Always work in a frozen copy with a forge project layout:

git clone <client-repo> audit-XYZ
cd audit-XYZ
git checkout <commit-hash>
forge install
forge build  # confirm clean build before touching anything
 
# Tooling skeleton
mkdir -p audit/{notes,slither,echidna,medusa,foundry-invariant,halmos,findings}

audit/findings/ will hold one .md per finding; audit/notes/ will hold your daily journal. Keep the audit branch separate from any patches.

5. Threat Modeling

5.1 STRIDE adapted to Web3

STRIDE was designed for enterprise software; mapping each category to smart-contract reality:

STRIDE	Classic meaning	Smart contract translation
S — Spoofing	Pretending to be someone else	Signature forgery / replay; `ecrecover` mis-checks; ERC-1271 bypass; impersonation via `tx.origin`; phishing-driven `permit`
T — Tampering	Modifying data in transit / at rest	Storage collision via `delegatecall`; oracle manipulation; mempool front-run reordering; calldata mutation; sandwich attacks
R — Repudiation	Denying an action took place	Missing events on critical state changes; events with wrong topics; events that can be spoofed
I — Information Disclosure	Leaking confidential data	”Private” variables visible in storage; secrets in calldata; off-chain commit-reveal failures; MEV searchers reading mempool
D — Denial of Service	Preventing legitimate use	Unbounded loops; gas griefing via 63/64 rule; revert-on-receive recipients in batched payouts; oracle staleness blocking liquidations
E — Elevation of Privilege	Gaining higher access than allowed	Uninitialized proxy initialize takeover; missing `onlyOwner`; missing access control on critical setters; role-collision in `AccessControl`; flash-loan governance

Run STRIDE per component. The output is a row in your threat model document.

5.2 Per-actor attacker model

Smart-contract attackers are not generic “users”. Enumerate them:

Actor	Capabilities	Constraints	Typical attack
Random user	Any external function with valid inputs	Limited capital	Bug-finding curiosity; rarely the primary threat
Sophisticated MEV searcher	Reads mempool, builds bundles, deploys helper contracts in same tx	Latency-sensitive; needs profit > gas	Sandwich, JIT liquidity, oracle race, liquidation race
Flash-loaner	Borrows millions atomically (Aave, Balancer, Maker), repays in same tx	Must close cycle profitably or revert	Oracle manipulation, governance vote, AMM imbalance
Governance attacker	Accumulates voting power (legitimate or via flash loan or borrow)	Subject to vote quorum/timelock	Beanstalk-style: pass malicious proposal that drains treasury
Insider / malicious admin	Has owner / multisig key	Bounded by timelock if any	Drain via privileged setter, swap oracle, rug pull
Oracle manipulator	Can move spot price on a thin DEX	Capital + slippage cost	TWAP manipulation if window is short; spot manipulation if used as primary feed
Compromised signer (1-of-N)	One key of a multisig leaked	N-1 honest signers	Requires social engineering or threshold mismatch
Frontend supply-chain attacker	Controls a JS dependency, CDN, DNS	Outside contract scope but in trust path	BadgerDAO-style malicious approval injection

For each actor, ask: what’s the worst they can do with what they have? That’s your threat row.

5.3 Trust boundaries

A trust boundary is a place where one trust assumption ends and another begins. Every boundary is a finding waiting to happen.

flowchart LR
    subgraph External[External / untrusted]
      U[User]
      MEV[MEV searcher]
      FL[Flash loaner]
    end
    subgraph Frontend[Frontend & infra<br/>trusted-ish]
      FE[Web UI]
      W[Wallet]
      RPC[RPC node]
    end
    subgraph Protocol[On-chain protocol]
      direction TB
      RT[Router]
      VT[Vault]
      OR[Oracle adapter]
    end
    subgraph Trusted[Trusted externals]
      CH[Chainlink]
      OZ[OZ libs]
      AAVE[Aave flashloan]
    end
    subgraph Admin[Admin path]
      MS[Multisig]
      TL[Timelock]
      GOV[Governor]
    end
    U --> FE --> W --> RPC --> RT
    RT --> VT
    VT --> OR --> CH
    GOV --> TL --> VT
    MS --> GOV
    AAVE -.borrows.-> RT
    style External fill:#ffe6e6
    style Frontend fill:#fff2cc
    style Protocol fill:#caffbf
    style Trusted fill:#a0c4ff
    style Admin fill:#d6c4ff

Each colored region has different trust. Boundaries between regions are exactly where to look hardest. The audit must enumerate every entry point that crosses a boundary and verify input validation, access control, and replay protection.

5.4 Threat model document template

# Threat Model — <Project>
Version: 0.1 · Date: <date> · Auditors: <names>
 
## 1. System overview
<one-paragraph description; reference architecture diagram>
 
## 2. Actors
| Actor | Capabilities | Trust level |
|-------|--------------|-------------|
| User  | call public functions, hold tokens | Untrusted |
| Keeper| call `liquidate()`, `rebalance()`  | Untrusted (liveness assumed) |
| Owner | call admin setters                 | Trusted within timelock window |
| ...
 
## 3. Trust boundaries
<diagram + textual list>
 
## 4. STRIDE per component
### Vault.sol
| Threat | Finding hypothesis | Mitigation present? | Verified |
|--------|-------------------|---------------------|----------|
| S — signature replay on `permit` | Possibly missing chainId binding | EIP-712 used | TBD |
| T — oracle price tamper          | Uses spot price on Uni V2        | TWAP? Chainlink? | TBD |
| ...
 
### Router.sol
...
 
## 5. Out-of-scope threats
- L1 reorg deeper than `finalized`
- Frontend supply-chain
- ...
 
## 6. Open questions for the client
- Is the keeper expected to be single-signer or multisig?
- What's the planned timelock duration?

Update this throughout the audit. By Day 10 every row should be Verified: yes/no + finding ID if applicable.

6. Invariant Identification

6.1 What is an invariant (precisely)

An invariant is a predicate over contract state that must hold true after every successful state transition, regardless of input. Examples:

“Total user balances equal address(this).balance in this vault.”
“totalShares > 0 implies totalAssets > 0.”
“A position is liquidatable iff healthFactor < 1e18.”
“After pause(), all state-changing entry points revert.”

Invariants are the specification of correctness. Bugs are violations of invariants the developer assumed but didn’t enforce.

6.2 How to find invariants

Three sources, in priority order:

The docs / spec / whitepaper. Explicit invariants like “the system is always solvent”. Quote them.
The test suite. Every assertion in tests is an implicit invariant. Lift them.
The code’s preconditions. Every require is an invariant the developer thought of. Inversely, every if (...) revert likewise. Note them and ask: is this list complete?

The hardest invariants are the ones no one wrote down — these are where the bugs live. To find them, ask: “if X stopped being true, what would break?” The breakable-but-unchecked things are your candidate invariants.

6.3 Invariant catalogue by protocol type

AMM (constant-product, e.g., Uniswap V2 fork)

#	Invariant	Why it matters
1	`reserveA * reserveB >= k_prev` after any swap (k can grow only via fees)	The whole pricing model; violation = drain
2	`LP_supply == 0` iff `reserveA == 0 && reserveB == 0`	Initial-mint integrity
3	Sum of LP shares = `LP_supply`	Accounting consistency
4	After `swap`, `balanceOf(this, tokenA) == reserveA + amountIn` exact	No “donations” trick the next swap
5	Skim/sync recover any token-balance overhang to LPs proportionally	No silent loss
6	`getReserves()` view matches `IERC20(tokenA).balanceOf(pool)` at end of every tx	Internal vs external accounting alignment

Lending market (Aave / Compound style)

#	Invariant
1	`sum(borrows) <= sum(collateral_USD_value * collateralFactor)` at the end of every tx
2	A position with `healthFactor < 1` is liquidatable by anyone
3	Liquidation is profitable for the liquidator (after-gas) when health factor is sufficiently below 1
4	Interest accrued on borrows >= interest paid to suppliers (after reserve factor)
5	Total supply of debt token == sum of individual user debts (with rounding tolerance)
6	Pause-state: no new borrows / no liquidations / withdrawals still allowed (or not — must match spec)
7	Per-asset cap (supply cap, borrow cap) never exceeded

ERC-4626 vault

#	Invariant
1	`convertToShares(convertToAssets(s)) ≈ s` (rounding direction documented)
2	`totalAssets() >= sum(deposit) − sum(withdraw)` (vault is solvent against deposits)
3	`previewDeposit` is monotone in `assets`
4	First depositor cannot extract value from later depositors via donation attack
5	Share price is monotone non-decreasing if yield strategy is non-losing
6	`maxRedeem(user) * sharePrice ≈ user.balance * sharePrice` (no surprise locks)

Bridge / cross-chain

#	Invariant
1	Tokens locked on chain A == tokens minted on chain B (per asset)
2	A given message hash can be executed at most once on the destination
3	Only events from `finalized` blocks on source result in destination action
4	Validator-set rotation requires N-of-M signature on the new set (no silent rotation)
5	Pause on either chain pauses the other (or matches spec)

6.4 Invariant catalogue document

# Invariants — <Project>
## Global
- G1: System is solvent: `sum(userBalances) == address(this).balance`
- G2: No tokens leave the system except via `withdraw()` or `liquidate()`
- G3: Paused implies all entry points except `unpause` and `emergencyWithdraw` revert
 
## Vault.sol
- V1: `totalAssets() >= totalDeposited - totalWithdrawn` (modulo profit)
- V2: `totalShares == 0` iff `totalAssets == 0` (or initial donation-attack mitigation in place)
- V3: `sharePrice` is monotone in time when strategy yields non-negative
 
## Router.sol
- R1: After a swap, no path tokens remain in Router (no dust accumulation)
- R2: Slippage bound is strictly enforced; revert path emits an event

Each invariant is a candidate for a fuzz target (§9.2) or a Certora rule (§10.2). The list itself is a deliverable — clients respond positively to “here is what we believed must always hold; here’s what fails”.

7. Manual Review

Manual review is where most bugs come from. Tools find easy bugs. Auditors find the hard ones. The art is in the passes.

7.1 Three passes

Pass 1 — Top-down (the user’s path)

Start at each external function. Follow it.

For each external function ask:

Who can call it? (modifiers, role checks, address checks)
What inputs must be valid? (bounds, non-zero, length caps)
What state does it read? (any of it stale? Any of it manipulated by the caller in the same tx?)
What state does it write? (correct order — CEI? Any unprotected writes that later code relies on?)
What external calls does it make? (reentrancy surface, return-data trust, gas behaviour)
What events does it emit? (sufficient to reconstruct off-chain? Correctly indexed?)
What’s the worst-case gas? (DoS for loops, gas grief in callbacks)
What changes if block.timestamp jumps 10 minutes? 1 day? block.number jumps 7200? (timestamp logic, expiry, accrual)

This is where 80% of findings emerge. Be patient. Aim for one external function fully reviewed per hour on first pass for complex code.

Pass 2 — Bottom-up (the state’s path)

For each state variable in storage, list every function that writes it. Then ask:

Is every writer access-controlled appropriately?
Are the writes consistent in semantics? (Two functions writing balance — do they both account for fees? For accruals?)
Is the initial value correct? (Critical for things like paused or feeBps — zero-initialized is fine for some, dangerous for others.)
Can it be set to a value outside the documented range? (E.g., feeBps > 10000?)

This pass catches what top-down misses: cross-function inconsistencies. “Both withdraw and liquidate reduce userBalance but liquidate forgets to update totalDeposits.”

Pass 3 — Cross-cutting

Patterns that span multiple files:

Access control matrix: every privileged function × every role. Excel-style. Any gaps? Any over-grants?
Event coverage: for each state-changing function, does it emit an event sufficient for off-chain reconstruction?
Modifier coverage: every onlyOwner/onlyRole usage. Any function that should have it but doesn’t?
Reentrancy surface: every external call. Does each path either use CEI or nonReentrant?
Math direction: every division. Rounds in protocol’s favor? In user’s favor? Consistent with documented direction?
Token interactions: every transfer/transferFrom/approve. SafeERC20? Handles return-data quirks?
Time logic: every use of block.timestamp/block.number. Manipulation surface? Sufficient granularity?

7.2 The diff-review (for re-audits)

When auditing a fix:

Read the issue you reported first. What was the bug?
Read the fix’s commit. Is the fix correct?
Read the rest of the diff — fixes often touch unrelated code or introduce new code. Audit the new code from scratch.
Re-run the fuzz harness that previously failed. Confirm it now passes (and that it’s the same harness, not a weakened one).
Confirm the invariant list still holds.

The single most-common re-audit failure: a fix that introduces a new bug. Treat the fix’s surface as fresh code.

7.3 Heuristics that fire fast

A “checklist of smells” — patterns where, when you see them, you stop and look carefully:

delegatecall to any address
assembly blocks
selfdestruct (post-Cancun: still relevant for legacy + initialization-window)
Inline ecrecover (vs ECDSA.recover)
abi.encodePacked(x, y, ...) where x or y are variable-length
Loops over arr.length where arr is user-controlled
transfer(addr, amt) not via SafeERC20
Custom math doing mulDiv by hand (vs FullMath / OZ Math)
Custom Merkle verification (vs OpenZeppelin.MerkleProof)
block.timestamp in pricing / oracle / randomness
block.number for time intervals (chain-dependent block time)
tx.origin anywhere
private/internal variables labeled as if they were secret
payable(addr).transfer(x) or .send(x) (legacy gas heuristic)
Cached DOMAIN_SEPARATOR in constructor
_disableInitializers() missing in upgradeable impl
Mappings with cleared keys but unused old data still readable

When any of these appears, the pace slows by 5×. Each is at the center of multiple historical exploits (cross-reference Tuan-05-Vulnerability-Classes-Part-1 and Tuan-06-Vulnerability-Classes-Part-2).

8. Static Analysis — Slither, Aderyn, and Custom Detectors

8.1 Why static analysis still matters

Tools cannot find economic, accounting, or cross-protocol bugs. They can find:

“You forgot to check this return value.”
“This delegatecall target is user-controlled.”
“This block.timestamp is used in randomness.”
“This contract has selfdestruct reachable from a public function.”

These are the boring bugs you should never miss. Running static analysis is the floor, not the work. But missing a Slither-findable bug in your audit is a credibility-shredding event.

8.2 Slither — the workhorse

What it is: Python-based static analyzer by Trail of Bits. ~100 detectors organized by severity (high / medium / low / informational / optimization) and confidence (high / medium / low).

Setup:

pip install slither-analyzer
# or pipx
pipx install slither-analyzer
 
slither --version  # confirm

Quick run on a Foundry project:

slither . --foundry-out-directory out --json slither.json --checklist > slither.md

This produces a Markdown checklist plus a JSON. Triage the Markdown: every finding either becomes a real finding in your report, or gets explicitly dismissed in your notes (with a reason).

Filter to a single detector:

slither . --detect reentrancy-eth,reentrancy-no-eth,reentrancy-events

Exclude noisy detectors:

slither . --exclude naming-convention,solc-version,pragma

Useful detector categories (sample, not exhaustive — full list in docs/detectors/):

Category	Notable detectors
High impact	`suicidal`, `uninitialized-state`, `arbitrary-send-eth`, `arbitrary-send-erc20`, `controlled-delegatecall`, `reentrancy-eth`
Medium	`reentrancy-no-eth`, `unchecked-transfer`, `weak-prng`, `tx-origin`, `incorrect-equality`, `dangerous-strict-equalities`
Low	`reentrancy-events`, `timestamp`, `divide-before-multiply`, `shadowing-local`
Informational	`naming-convention`, `solc-version`, `assembly`

Printer modules — for codebase comprehension, not bug-finding:

slither . --print human-summary       # high-level: contracts, inheritance, complexity
slither . --print contract-summary    # per-contract: functions, state vars, modifiers
slither . --print call-graph          # DOT call graph
slither . --print inheritance-graph   # DOT inheritance graph
slither . --print function-summary    # per-function: callers, callees, modifiers, state writes
slither . --print modifiers           # all modifiers in scope
slither . --print loc                 # SLOC counts
slither . --print entry-points        # external/public surface

The first thing to do on an unknown codebase: slither --print human-summary,contract-summary,entry-points. It is a free reading of the codebase’s shape.

CI integration:

# .github/workflows/slither.yml
name: Slither
on: [pull_request]
jobs:
  slither:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: crytic/[email protected]
        with:
          fail-on: high
          sarif: results.sarif
      - uses: github/codeql-action/upload-sarif@v3
        with: { sarif_file: results.sarif }

fail-on: high blocks merges on high-severity findings; SARIF upload puts results into the GitHub Security tab.

8.3 Custom Slither detectors

When a project has a specific anti-pattern (e.g., “any function that changes oracle must have onlyOwner”), write a custom detector.

Skeleton (~50 lines):

# detectors/oracle_setter_acl.py
from slither.detectors.abstract_detector import AbstractDetector, DetectorClassification
 
class OracleSetterAcl(AbstractDetector):
    """
    Flags any function that writes to `oracle` storage but is missing onlyOwner.
    """
    ARGUMENT = "oracle-setter-acl"
    HELP = "Functions that modify the oracle must be onlyOwner"
    IMPACT = DetectorClassification.HIGH
    CONFIDENCE = DetectorClassification.MEDIUM
    WIKI = "https://example.com/oracle-acl"
    WIKI_TITLE = "Unprotected oracle setter"
    WIKI_DESCRIPTION = "Any function that modifies the `oracle` address must be access-controlled."
    WIKI_EXPLOIT_SCENARIO = "Attacker swaps oracle to one they control; drains protocol via mispriced trades."
    WIKI_RECOMMENDATION = "Add `onlyOwner` (or equivalent role check) to all oracle-setting functions."
 
    def _detect(self):
        results = []
        for contract in self.compilation_unit.contracts_derived:
            for f in contract.functions_entry_points:
                # find writes to a state variable named `oracle`
                writes_oracle = any(
                    sv.name == "oracle" for sv in f.state_variables_written
                )
                if not writes_oracle:
                    continue
                # check modifiers / require statements
                has_acl = any(m.name in ("onlyOwner", "onlyRole", "onlyAdmin") for m in f.modifiers)
                if not has_acl:
                    info = [f, " modifies `oracle` without access control\n"]
                    results.append(self.generate_result(info))
        return results

Run:

slither . --detect oracle-setter-acl --detectors-paths detectors/

This is the most valuable static-analysis investment per audit: 30 minutes writing a project-specific detector catches the same class of bug everywhere it appears.

8.4 Aderyn (Cyfrin) — Rust alternative

What it is: Rust-based static analyzer, ~100 detectors (as of 2026 — [verify]). Faster startup than Slither; integrates well with Foundry; produces Markdown, JSON, and SARIF reports.

cargo install aderyn  # or brew install cyfrin/tap/aderyn
aderyn .              # writes report.md by default

Aderyn’s coverage overlaps with Slither but isn’t identical. Some detectors are stricter or more recent. Run both on every codebase — they disagree usefully. A finding flagged by one and not the other is worth a closer look.

8.5 Solhint — style + light security

What it is: ESLint-style linter for Solidity. Catches style violations and a small set of security smells.

npm i -D solhint
npx solhint 'src/**/*.sol'

Don’t rely on it for security. Useful for CI to catch obvious style drift; for security, defer to Slither / Aderyn.

8.6 Mythril, Manticore — legacy

Both still exist; Mythril is occasionally useful as a third opinion on small contracts. Manticore’s maintenance status is uncertain in 2026 [verify]. Don’t make either your primary tool.

8.7 SWC Registry — historical reference

The Smart Contract Weakness Classification (SWC) registry is partially deprecated — IDs are still cited in older reports, but the registry isn’t actively maintained. Use it as a shared vocabulary with older reports (SWC-107 = reentrancy, SWC-101 = integer overflow, etc.) but rely on OWASP SC Top 10 (2025) or the auditor’s own catalog for current taxonomy.

9. Fuzzing — Echidna, Medusa, Foundry Invariant

9.1 Why fuzz

Static analysis answers “is there a pattern in the code?“. Fuzzing answers “does the contract violate a property under any input sequence?“. The two are complementary:

Static: covers all paths but only patterns the detector knows.
Fuzz: covers only paths exercised but discovers unknown property violations.

Fuzzing is where invariants become tests. Every invariant from §6 is a candidate property.

9.2 Echidna

What it is: Haskell-based property fuzzer by Trail of Bits. Coverage-guided, persistent corpus, integrates with crytic-compile (so it understands Foundry projects).

Property mode:

// test/echidna/EchidnaVault.sol
contract EchidnaVault is Vault {
    // Echidna calls all public functions; we add property_*
    function echidna_total_supply_matches_assets() public view returns (bool) {
        return totalSupply() == 0 || totalAssets() > 0;
    }
 
    function echidna_share_price_monotone() public view returns (bool) {
        return _sharePrice() >= _lastSharePrice;
    }
}

Assertion mode:

function deposit(uint256 amt) public {
    uint256 priceBefore = _sharePrice();
    _deposit(amt);
    uint256 priceAfter = _sharePrice();
    assert(priceAfter >= priceBefore);  // Echidna catches the failure
}

Config:

# echidna.yaml
testMode: assertion        # or "property"
seqLen: 100                # tx sequence length per test
testLimit: 100000          # iterations
corpusDir: corpus/         # persistent across runs
coverage: true             # coverage-guided generation
shrinkLimit: 5000          # shrinking effort
prefix: "echidna_"         # property prefix
balanceContract: 0xffffffff
balanceAddr:     0xffffffff
filterFunctions: []
filterBlacklist: true

Run:

echidna test/echidna/EchidnaVault.sol --contract EchidnaVault --config echidna.yaml

What it’s good at:

Stateful sequences (tx1 → tx2 → tx3) that violate a property at the end.
Discovering subtle invariant violations involving rounding, accumulation, edge values.
Coverage-guided exploration — it finds branches you’d never write a test for.

Limitations:

Slow on large surfaces. Reduce by filterFunctions and constrained handlers.
Can’t easily reason about external protocols on a mainnet fork (use Medusa for fork tests).
Property mode requires echidna_* view functions; assertion mode is more flexible.

9.3 Medusa

What it is: Go-based fuzzer by Trail of Bits — “Echidna 2.0”. Coverage-guided, mutational, parallel across workers, built on go-ethereum so it can fork mainnet.

Config (medusa.json):

{
  "fuzzing": {
    "workers": 10,
    "workerResetLimit": 50,
    "timeout": 0,
    "testLimit": 0,
    "callSequenceLength": 100,
    "corpusDirectory": "medusa-corpus",
    "coverageEnabled": true,
    "targetContracts": ["EchidnaVault"]
  },
  "compilation": {
    "platform": "crytic-compile",
    "platformConfig": { "target": "." }
  },
  "testing": {
    "assertionTesting": { "enabled": true },
    "propertyTesting": { "enabled": true, "testPrefixes": ["echidna_", "medusa_"] },
    "optimizationTesting": { "enabled": false }
  }
}

Run:

medusa fuzz

Use Medusa over Echidna when:

You need parallelism (multi-core wallets).
You need mainnet fork testing (go-eth-fork mode).
You want a single config that runs both property and assertion modes.

Use Echidna over Medusa when:

You’re using the older property-only mode and have an Echidna-specific corpus already.
You prefer Haskell’s slightly different sequence-shrinking behavior on specific bug shapes.

In practice as of 2026, Medusa is the more active default; Echidna remains supported. Run both on critical contracts — corpus sharing means each can warm-start the other.

9.4 Foundry invariant testing — handler pattern

What it is: invariant tests built into forge test. Runs random sequences against targetContracts, then evaluates invariant_* functions.

Naive (anti-pattern) invariant:

contract VaultInvariants is Test {
    Vault vault;
    function setUp() public { vault = new Vault(...); targetContract(address(vault)); }
    function invariant_solvent() public view {
        assert(vault.totalAssets() >= vault.totalDeposited());
    }
}

Problem: with vault as direct target, the fuzzer calls arbitrary functions with arbitrary parameters — most reverts; coverage is shallow.

Handler pattern:

// test/invariant/VaultHandler.sol
contract VaultHandler is Test {
    Vault public vault;
    MockToken public asset;
    address[] public actors;
    address internal currentActor;
 
    // Ghost state
    uint256 public ghost_depositSum;
    uint256 public ghost_withdrawSum;
    mapping(address => uint256) public ghost_perActorDeposits;
 
    modifier useActor(uint256 actorSeed) {
        currentActor = actors[bound(actorSeed, 0, actors.length - 1)];
        vm.startPrank(currentActor);
        _;
        vm.stopPrank();
    }
 
    constructor(Vault _v, MockToken _a) {
        vault = _v; asset = _a;
        for (uint i = 0; i < 5; i++) actors.push(address(uint160(0x1000 + i)));
    }
 
    function deposit(uint256 actorSeed, uint256 amt) external useActor(actorSeed) {
        amt = bound(amt, 1, 1e24);
        asset.mint(currentActor, amt);
        asset.approve(address(vault), amt);
        vault.deposit(amt, currentActor);
        ghost_depositSum += amt;
        ghost_perActorDeposits[currentActor] += amt;
    }
 
    function withdraw(uint256 actorSeed, uint256 shares) external useActor(actorSeed) {
        uint256 max = vault.maxRedeem(currentActor);
        if (max == 0) return;
        shares = bound(shares, 1, max);
        uint256 assets = vault.redeem(shares, currentActor, currentActor);
        ghost_withdrawSum += assets;
    }
 
    function donate(uint256 amt) external {
        amt = bound(amt, 1, 1e24);
        asset.mint(address(this), amt);
        asset.transfer(address(vault), amt);  // simulate donation attack
    }
 
    function getActors() external view returns (address[] memory) { return actors; }
}

// test/invariant/Vault.invariant.t.sol
contract VaultInvariantTest is Test {
    Vault vault;
    VaultHandler handler;
 
    function setUp() public {
        MockToken asset = new MockToken();
        vault = new Vault(address(asset));
        handler = new VaultHandler(vault, asset);
        targetContract(address(handler));
 
        // Restrict to handler functions only
        bytes4[] memory selectors = new bytes4[](3);
        selectors[0] = VaultHandler.deposit.selector;
        selectors[1] = VaultHandler.withdraw.selector;
        selectors[2] = VaultHandler.donate.selector;
        targetSelector(FuzzSelector({ addr: address(handler), selectors: selectors }));
    }
 
    function invariant_solvent() public view {
        assertGe(
            vault.totalAssets(),
            handler.ghost_depositSum() - handler.ghost_withdrawSum(),
            "vault not solvent"
        );
    }
 
    function invariant_share_price_monotone() public {
        // ghost var tracks lastSharePrice, asserted in handler
    }
 
    function invariant_no_dust() public view {
        // Router-level
    }
 
    function invariant_callSummary() public view {
        console.log("deposits:",   handler.ghost_depositSum());
        console.log("withdraws:",  handler.ghost_withdrawSum());
    }
}

Key config (foundry.toml):

[invariant]
runs = 256
depth = 100
fail_on_revert = false        # set true once handler is fully bounded
shrink_run_limit = 5000
call_override = false

Best practices:

Always use a handler. Direct-target fuzzing of business contracts is shallow.
bound(x, lo, hi) every fuzz input to valid ranges; don’t use vm.assume (it discards rather than maps).
Ghost variables capture cumulative on-chain state the contract doesn’t store directly.
fail_on_revert = false during exploration; flip to true once handlers properly bound inputs.
invariant_callSummary prints per-run call distribution — verify the fuzzer actually exercises the surface.
targetSelector / excludeSelector to keep the fuzzer focused.

9.5 Fuzzer comparison — what each catches

Property	Echidna	Medusa	Foundry invariant
Stateful sequences	Yes	Yes	Yes
Property mode (`property_*`)	Yes	Yes	No (uses `invariant_*`)
Assertion mode	Yes	Yes	Yes (in handler)
Coverage-guided	Yes	Yes	Limited
Persistent corpus	Yes	Yes	No
Mainnet fork	Limited	Yes	Yes (via vm.createSelectFork)
Parallel	No (single-threaded)	Yes	No
Ergonomic for Solidity devs	Medium	Medium	High
Speed (vs same-codebase Foundry)	Faster on long sequences	Fastest with parallelism	Slowest, best DX

Practical rule: write your invariants once as Foundry invariant_* tests (for DX), then port the same properties to Echidna/Medusa for deeper coverage runs (overnight). Same harness, two engines.

10. Symbolic Execution & Formal Verification

10.1 Halmos — Foundry-compatible symbolic checks

What it is: a16z’s symbolic test runner. Reads Foundry-style tests; runs them with symbolic inputs rather than concrete ones. Uses bounded model checking — it exhaustively explores all paths up to a bound.

Setup:

uv tool install halmos
# or: pip install halmos
halmos --help

Test convention — same as Foundry, with check_* or test_* prefix:

// test/halmos/CheckVault.t.sol
import "forge-std/Test.sol";
import "halmos-cheatcodes/SymTest.sol";
import "../../src/Vault.sol";
 
contract CheckVault is SymTest, Test {
    Vault vault;
 
    function setUp() public {
        vault = new Vault(address(new MockToken()));
    }
 
    function check_deposit_increases_total(uint256 amt) public {
        vm.assume(amt > 0 && amt < type(uint128).max);
        uint256 before = vault.totalAssets();
        vault.deposit(amt, msg.sender);
        uint256 after_ = vault.totalAssets();
        assert(after_ >= before + amt - 1);  // -1 for rounding
    }
 
    function check_arbitrary_sequence() public {
        address user = svm.createAddress("user");
        uint256 a = svm.createUint256("a");
        uint256 b = svm.createUint256("b");
        vm.assume(a + b > 0);
        // Halmos explores all (a, b) and all symbolic users
        vault.deposit(a, user);
        vault.deposit(b, user);
        assert(vault.balanceOf(user) > 0);
    }
}

Run:

halmos --function check_  --loop 4 --solver-timeout-assertion 60000

Strengths:

Symbolic — proves properties hold for all inputs, not just sampled ones.
Foundry-native — reuse your test harness.
Catches the “edge case the fuzzer never hit” by construction.

Limitations:

Loops: bounded; if your code has a 100-iter loop, Halmos must be told to unroll N times. Beyond bound = unsound coverage.
External calls to unknown code: Halmos may not be able to model them precisely; use mocks.
State explosion: complex state (many storage vars, deep state machines) makes Halmos slow or timeout.
Not a replacement for fuzzing or Certora — it’s the middle ground.

Where Halmos shines:

Pure-math libraries (TickMath, FullMath, fixed-point arithmetic) — proves no overflow/underflow under all inputs.
Access control matrices — prove “function X reverts unless caller has role Y” symbolically.
Single-tx invariants — prove a function’s pre/post relationship for all symbolic inputs.

10.2 Certora Prover — heavyweight formal verification

What it is: a commercial-grade SMT-backed verifier. You write specifications in CVL (Certora Verification Language); the prover proves or disproves them against the Solidity bytecode.

CVL primer:

// vault.spec
methods {
    function totalAssets() external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
    function deposit(uint256, address) external returns (uint256);
    function redeem(uint256, address, address) external returns (uint256);
}
 
// Invariant: zero supply iff zero assets
invariant totalSupplyZeroIffTotalAssetsZero()
    totalSupply() == 0 <=> totalAssets() == 0;
 
// Rule: deposit increases caller's shares
rule depositIncreasesShares(uint256 amt, address rcv) {
    env e;
    require amt > 0;
    require rcv != currentContract;
 
    uint256 sharesBefore = balanceOf(rcv);
    deposit(e, amt, rcv);
    uint256 sharesAfter = balanceOf(rcv);
 
    assert sharesAfter > sharesBefore, "shares must increase";
}
 
// Ghost tracking total flow
ghost mathint totalDeposited;
hook Sstore deposits[KEY address user] uint256 newVal (uint256 oldVal) {
    totalDeposited = totalDeposited + newVal - oldVal;
}
 
// Rule using the ghost
invariant solvency()
    to_mathint(totalAssets()) >= totalDeposited;

Concepts (more in Tuan-Bonus-Formal-Verification-Deep):

Methods block: declares external functions and their abstraction (envfree = no env dependency).
Rules: parameterised properties checked over symbolic inputs.
Invariants: properties that must hold in every reachable state — proved by induction.
Ghosts: shadow storage variables Certora maintains, mirrored to real state via hooks.
Hooks: code that runs on SLOAD / SSTORE / CALL — like instrumentation.
Parametric rules: rules quantified over methods (one rule covers “every function preserves invariant X”).
Sanity checks: built-in checks that rules aren’t vacuous.

Run (via certora-cli):

pip install certora-cli
certoraRun src/Vault.sol --verify Vault:certora/vault.spec --solc solc-0.8.24 --rule depositIncreasesShares

Cost / availability:

Commercial product. Free tier exists (limited compute). Engagements with the Certora team are typically priced per protocol.
Most independent auditors don’t have Certora budget on every audit. It shows up on top-tier engagements (Aave, Compound, Maker, Lido, etc.).

Strengths over Halmos:

Inductive invariants — can prove statements over unbounded loops/state.
Mature counterexample reporting.
Industry track record on big protocols.

Limitations:

Steep learning curve. Plan 1–2 weeks just to become productive in CVL.
SMT timeouts on complex spec — refactoring the spec to be SMT-friendly is its own skill.
Cost / access.

10.3 K framework — for the truly motivated

Rosario / Runtime Verification’s K framework can model the EVM itself (KEVM) and verify properties against a semantic model. Used in: Uniswap V1 formal proof, Casper FFG specification, Beacon Chain. Far heavier than Certora; usually reserved for protocol-level rather than application-level work. Out of scope for routine audits.

10.4 When to reach for symbolic/formal

Question	Tool
”Does this math library never overflow?”	Halmos
”Is the access-control matrix complete?”	Halmos
”Is the system solvent under any sequence of users?”	Certora invariant
”Does any upgrade path preserve the storage layout?”	Certora rule (or OZ upgrades-plugin static check)
“Is the consensus algorithm sound?”	K / Coq (research-grade)
“Does the spec describe the implementation?”	Certora rule (one per spec clause)

Fuzz first (cheap), then symbolic (deeper coverage), then formal (proof-grade). Don’t skip fuzz to go straight to Certora — you’ll waste expensive prover time on properties that fuzz would have falsified in seconds.

11. Differential & Fork Testing

11.1 Differential testing

When the protocol is a fork of a known-good reference (Uniswap V2 fork, Compound fork, ERC-4626 reference), compare against the reference:

contract DiffTest is Test {
    UniswapV2Fork forkedPool;
    UniswapV2Reference refPool;
 
    function setUp() public {
        forkedPool = new UniswapV2Fork(tokenA, tokenB);
        refPool = new UniswapV2Reference(tokenA, tokenB);
        // mirror init state
    }
 
    function test_diff_swap(uint256 amt) public {
        amt = bound(amt, 1, 1e24);
 
        uint256 forkedOut = forkedPool.swap(amt);
        uint256 refOut = refPool.swap(amt);
        assertEq(forkedOut, refOut, "fork diverges from reference");
    }
}

Any divergence is either a deliberate improvement (which the docs must call out and you must check) or an unintended bug.

11.2 Fork testing — production state as fixture

vm.createSelectFork(rpcUrl, blockNumber) lets a Foundry test run against actual mainnet state. Critical for:

Integration verification: does your contract behave correctly against the real Curve pool, not a mock?
Replay of historical exploits: fork the block before the exploit; run the attack; confirm reproduction.
Upgrade simulation: fork mainnet, run the upgrade transaction, then run the test suite against post-upgrade state.

function setUp() public {
    vm.createSelectFork(vm.envString("MAINNET_RPC"), 18_500_000);
    vault = Vault(0x...real address...);
}
 
function test_invariant_against_mainnet() public {
    // Real-state invariant check
    assertGe(vault.totalAssets(), vault.totalDeposited());
}

Useful caveat: a fork is slow — each RPC call is a network round-trip. Use --fork-block-number to pin and locally-cached RPCs (anvil --fork-url with local cache) where possible.

12. Economic Risk Analysis

12.1 The non-code attack surface

Not every bug is a code bug. Some are economic — the code does exactly what it says, but the incentive structure lets an attacker profit by manipulating it.

Cross-reference Tuan-09-Oracle-MEV-Economic-Attack for the deep treatment. For the methodology week, the checklist:

Oracle: what’s the cost to move the price 1% on the source the protocol reads? Is it cheaper than the protocol’s TVL × max-extract per tx?
Liquidation: is liquidating always profitable after gas? In what market conditions does it become unprofitable? (When liquidations stop, bad debt accumulates.)
Flash-loan amplification: assume an attacker can borrow $1 B a t o mi c a ll y f or$ 0 cost. What can they do in one tx with $1 Bt ha tt h eyco u l d n^{'} tw i t h$ 0?
Governance: how much voting power costs how much capital? Can it be flash-loaned? Is there a timelock long enough to defend?
MEV: which functions are sandwichable? Which create JIT-liquidity opportunities? Which provide search-able information via emitted events?
Fee bound: can fees ever exceed 100% (rounding bugs)? Can fees go negative (subsidies via rounding)?
Bad debt socialization: when a position is underwater after liquidation, who eats the loss? Documented?

12.2 Modeling

Economic findings need numbers. The audit report should say:

“At a price of $1, 800/ ET H, ana tt a c k erco n t ro ll in g$ 5M of capital can flash-loan an additional $200 M o f W ET Ho n A a v e, s w a p o n U ni s w a p V 2 W ET H / U S D Cp oo l (w h osereser v es a re$ 8M as of block X), move the spot price by ~25%, exploit the protocol’s spot-price oracle to mint $40 M o f s t ab l eco ina g ain s t$ 10M of collateral, repay the flash loan, and walk away with ~$30M net. PoC in test/Exploit.t.sol.”

Numbers tied to mainnet block state make a finding undeniable. Numbers tied to “in theory” are downgrade-fodder for the client.

13. Severity Classification

13.1 The three dominant rubrics

Rubric	Used by	Tiers	Stance
Immunefi v2.3	Immunefi bug bounties (large fraction of mainnet bounties)	Critical / High / Medium / Low	Impact-led; likelihood is a downgrade modifier
Code4rena	Code4rena contests, also widely adopted by independents	High / Medium / Low / Q&A	Impact × likelihood; judge discretion
Sherlock	Sherlock contests	High / Medium only (Low / informational not paid)	Strict impact bands; likelihood NOT considered

These are not always interchangeable. When writing a private audit report, pick one rubric, name it in the methodology section, and apply it consistently. The most common choice in private engagements is the Code4rena rubric (familiar to clients, expressive on Low/Q&A).

13.2 Immunefi V2.3 (smart contract — impact based)

Tier	Smart contract examples
Critical	Direct theft of user funds; permanent freezing of funds; unauthorized minting of NFTs/tokens; protocol insolvency; governance vote manipulation
High	Theft / freezing of unclaimed yield, royalties; temporary freezing of funds (recoverable); theft of gas
Medium	Contract fails under specific edge-case state; griefing (non-trivial cost to attacker, non-trivial damage); block-stuffing for profit; unbounded gas consumption
Low	Contract fails to deliver promised returns but doesn’t lose value

Reward for critical contract bugs on Immunefi-bountied programs: 10% of the funds-at-risk, capped at $1M (varies per project). Other bounty venues have other caps.

Modifiers (downgrade conditions):

Privileged role required: bug requires admin to act — downgrade unless admin compromise is the threat.
User interaction required: bug requires a user to sign / submit something they wouldn’t normally — partial downgrade.
External condition required: bug requires a specific oracle state, market state, or attacker capital threshold — partial downgrade based on how realistic the condition is.

13.3 Code4rena rubric

Tier	Rule of thumb
High (H)	Assets can be stolen, lost, or compromised directly; or there’s a valid attack path with realistic assumptions
Medium (M)	Assets not at direct risk; protocol function / availability impacted; value can leak under stated external assumptions
Low (L)	Findings worth knowing but not exploitable; design improvements
Q&A	Style / informational / gas-opt; not security-relevant per se

Burden of proof on the warden (finder): the more severe, the better the PoC + impact rationale must be.

C4 explicitly considers impact × likelihood. A High-impact / Low-likelihood bug may be judged Medium. A Medium-impact / High-likelihood bug may be judged Medium. Judge discretion.

13.4 Sherlock rubric (strict)

Sherlock only pays out High and Medium:

High: Direct loss of funds without (extensive) external conditions; loss is >1% AND > $10 o f p r in c i p a l / y i e l d, or p ro t oco ll oses > 1$ 10 of fees.
Medium: Loss of funds requiring specific conditions; or breaks core functionality; loss thresholds >0.01% AND >$10.

Notably: Likelihood is not considered for validity. If an attack is theoretically possible and meets the impact bar, it’s valid even if difficult to execute.

Sherlock-specific rules:

Admin functions assumed used correctly unless the contest README says otherwise.
DoS: funds locked >7 days OR time-sensitive function impacted = Medium. Both = High.
Front-running on public mempool chains is in-scope; on private-mempool chains (Arbitrum, Optimism, etc.), front-running is out-of-scope.
Storage-gap omissions usually invalid (unless complex inheritance).
Stale-Chainlink-price reports are typically invalid unless paired with a clear consumer impact.

13.5 Defending severity to the client

Clients argue for downgrades. They will. Be prepared:

Client argument	Counter
”It requires admin compromise"	"Admin compromise is a documented risk in your threat model. If admin compromise leads to user fund loss, that’s at least High. Per Immunefi, admin-only is a downgrade modifier, not an automatic Low."
"An attacker would need $50M to execute"	"Flash loans exist. $50 M i s a v ai l ab l e v ia A a v e f or$ 0 cost. Find me a credible barrier and we’ll revisit."
"It would be obvious on-chain and we could pause"	"Pause-response assumes you’re awake when the tx lands. Has the team done an incident drill? What’s your detection lag?"
"The user has to sign something they wouldn’t normally"	"Phishing is real. Wallet drainers run 24/7 on every approval flow. User-action-required is a partial modifier, not an automatic Low."
"It’s not in this audit’s scope"	"Acknowledged. Documenting as out-of-scope finding for your records; recommending follow-up audit."
"We’re going to fix it before launch"	"Fine — severity is what it would be on the code in scope. Fix removes the finding, not the severity.”

The auditor’s job is integrity under pressure. If you downgrade severity to keep a client happy and the protocol gets hacked at the severity you originally assigned, your name is in the post-mortem.

13.6 Likelihood = capital + access + complexity

A practical likelihood model when you need one:

likelihood = capital_score × access_score × complexity_score
where
  capital_score   ∈ {0.1: needs >$10M sustained ; 0.5: needs flash-loan capacity ; 1.0: any user}
  access_score    ∈ {0.1: needs admin ; 0.3: needs whitelisted role ; 0.5: needs lp / borrower ; 1.0: any caller}
  complexity_score ∈ {0.3: requires multi-tx + specific block timing ; 0.7: single-tx complex ; 1.0: single-tx trivial}

Multiply, bucket into High/Med/Low likelihood. Combine with impact for final severity.

This is not a rubric to publish in reports — it’s an internal heuristic. Final severity in the report uses the rubric you adopted.

14. Tooling Setup — All-in-one Foundry Project

The full toolchain on one project. Reproducible setup:

# Foundry baseline
curl -L https://foundry.paradigm.xyz | bash
foundryup
 
# Slither
pipx install slither-analyzer
 
# Echidna (Mac)
brew install echidna
# (Linux) curl -L https://github.com/crytic/echidna/releases/latest/download/echidna-test-2.3.2-Linux.tar.gz | tar xz
 
# Medusa
go install github.com/crytic/medusa/cmd/medusa@latest
# or brew install medusa
 
# Halmos
uv tool install halmos
 
# Aderyn
cargo install aderyn
 
# Solhint
npm i -g solhint
 
# Certora (optional; requires account)
pip install certora-cli
# Provide CERTORAKEY env var

Project layout for an audit:

audit-<project>/
├── foundry.toml
├── slither.config.json
├── echidna.yaml
├── medusa.json
├── certora/
│   ├── *.spec
│   └── conf/*.conf
├── detectors/                 # custom Slither detectors
├── src/                       # client code, frozen
├── test/
│   ├── unit/                  # reproduction of bugs as you find them
│   ├── invariant/             # Foundry invariant + handler
│   ├── echidna/               # property contracts for Echidna/Medusa
│   ├── halmos/                # check_* symbolic tests
│   └── fork/                  # mainnet-fork integration tests
├── audit/
│   ├── scoping.md
│   ├── threat-model.md
│   ├── invariants.md
│   ├── notes/                 # daily journal
│   ├── findings/              # one .md per finding
│   └── tooling-output/        # slither.md, aderyn.md, fuzz logs
└── README.md                  # audit-specific README pointing at the deliverables

foundry.toml:

[profile.default]
src = "src"
out = "out"
libs = ["lib"]
solc = "0.8.24"
optimizer = true
optimizer_runs = 200
via_ir = false
 
[profile.default.fuzz]
runs = 10000
seed = "0x1"
 
[profile.default.invariant]
runs = 256
depth = 200
fail_on_revert = false
shrink_run_limit = 5000
 
[fmt]
line_length = 100

CI: run forge test, forge coverage, slither --fail-on high, aderyn on every PR. Save artifacts.

15. Tenderly — Simulation, Debugging, Monitoring

15.1 Use cases

Simulate a transaction before submitting it (front-run-safe; auditors use it to preview a fix).
Debug a failed tx with full opcode-level trace and decoded inputs.
Forks: spin up a private fork of mainnet, run scenarios, share with the client.
Alerts / Web3 Actions: trigger an off-chain notification when an on-chain invariant fails (e.g., paused unexpectedly, balance drops below threshold).

15.2 Audit workflow with Tenderly

Reproducing a historical exploit: paste the tx hash; Tenderly shows the full trace decoded. Useful to learn from real incidents and to confirm your PoC matches the historical attack.
Pre-deploy verification: simulate the protocol’s first user flow against the fork; confirm no unexpected reverts.
Post-deploy monitoring (with the client): set up alerts on critical invariants (“total supply > 0”, “no unexpected admin call to setOracle”). Hand over as a deliverable.

Cost: free tier exists; paid tiers for team / monitoring features. Most audit engagements include “set up monitoring” as a soft deliverable.

15.3 Alternative tooling

Phalcon / Blocksec Explorer: excellent for tracing historical exploits.
Forta: real-time monitoring with community-built detection bots.
OpenZeppelin Defender: monitoring + admin workflows.

A modern audit report typically recommends specific monitoring rules. Treat monitoring as part of the deliverable, not an extra.

16. Findings Consolidation

16.1 The running findings journal

During manual review, every potential issue goes into a finding file even if uncertain:

audit/findings/F-001-unprotected-oracle-setter.md
audit/findings/F-002-readonly-reentrancy-virtualPrice.md
audit/findings/F-003-rounding-direction-favors-user.md
...

Status tags inside each file:

Status: Draft — being investigated.
Status: Confirmed — PoC works.
Status: Won't-fix — false positive, with reason.
Status: Reported — included in the report.

By Day 8 every Draft is either Confirmed-Reported or Won’t-fix.

16.2 Deduplication

Two findings that share root cause = one finding with two manifestations. Two findings that share manifestation but differ in root cause = two findings.

Example: a single missing access control on setOracle is one finding even if there are three external entry points that all reach it.

16.3 Severity calibration

Once findings are confirmed, do a calibration pass:

List all findings with proposed severities.
Re-read the rubric (Immunefi / C4 / Sherlock — whichever you picked).
Compare findings against each other: is finding A really more severe than finding B? If they’re plausibly equal, are you assigning them the same severity?
Look for outliers — a single Critical or single Low among Medium-heavy reports is suspicious. Either justify it explicitly or re-evaluate.

16.4 Finding template (preview of Week 16)

# F-002 — Read-only reentrancy in `Vault.virtualPrice()`
Severity: **High**
Status: Confirmed
Detected by: Manual review + Foundry PoC
 
## Summary
`Vault.virtualPrice()` returns mid-transition state during `removeLiquidity()`, allowing
external protocols that consume this view as an oracle to be drained.
 
## Detail
`removeLiquidity()` updates `totalAssets` after an external call to the user (line 142).
A view function `virtualPrice()` reads `totalAssets / totalShares`. During the external
call, `totalShares` has been decremented but `totalAssets` has not. A malicious user's
`receive()` fallback can call into a consumer protocol (Bank.sol) that reads
`virtualPrice()` at this moment and mis-prices a deposit.
 
## PoC
`test/exploit/ReadOnlyReentrancy.t.sol` — drains 100 ETH from `Bank.sol` in a single tx.
 
## Impact
Up to TVL of any external consumer protocol using `Vault.virtualPrice()` as an oracle.
At time of audit, two known integrators on testnet; mainnet impact depends on adoption.
 
## Recommendation
Apply `nonReentrant` to view functions used as oracles, or move the external call after
state finalization in `removeLiquidity()`. Document the oracle-safe view explicitly in
NatSpec.
 
## References
- [Curve readonly-reentrancy archetype](https://chainsecurity.com/heartbreaks-curve-lp-oracles/)
- Tuan-05 lesson §2.2.4

This template detail is the Week 16 focus; here we just confirm the shape.

17. Remediation Review

17.1 What remediation review is

After the client ships fixes, you audit the fixes. Not the same as a fresh audit — narrower scope, but with new risks:

Did the fix close the original bug?
Did the fix introduce a new bug?
Did the fix change semantics beyond the bug? (e.g., a fix that “fixed” reentrancy by adding a refund flow that itself has a different bug)
Are tests added that lock in the fix?

17.2 Deliverable

A short “Remediation Report” companion to the main report:

# Remediation Review — <Project>
Date: <date>  Commit: <new SHA>  Prior commit: <old SHA>
 
## Findings status
| ID | Original severity | Status | Notes |
|----|-------------------|--------|-------|
| F-001 | High | **Fixed** | Patch in commit abc123; verified via `test_F001_fixed` |
| F-002 | High | **Fixed (partial)** | Patch addresses two of three call-sites; third (Module.sol:201) still vulnerable |
| F-003 | Medium | **Acknowledged** | Client chose to document as known limitation |
| F-004 | Low | **Fixed** | |
 
## New findings discovered during remediation review
| ID | Severity | Summary |
|----|----------|---------|
| F-007 | Medium | Fix to F-001 introduced rounding that favors user on tiny deposits |
 
## Conclusion
3 of 4 original findings fully remediated. 1 partial fix outstanding (F-002). 1 new finding
introduced (F-007). Recommend further fix-and-review cycle before launch.

The first time a client tries to launch with “partial” or “new finding introduced” status on a Medium-or-above is the moment your job earns its fee. Hold the line.

18. Lab — Tooling Bake-off + Mock Audit + Custom Detector

18.1 Setup

mkdir -p ~/web3-sec-lab/wk15 && cd ~/web3-sec-lab/wk15
forge init audit-tooling-lab
cd audit-tooling-lab
 
# Install everything (re-run from §14)
pipx install slither-analyzer
brew install echidna medusa
uv tool install halmos
cargo install aderyn
 
# Configs
touch echidna.yaml medusa.json slither.config.json
mkdir -p detectors test/{unit,invariant,echidna,halmos,fork} audit/{notes,findings}

18.2 Lab 1 — Tooling bake-off on a known-vulnerable contract

Use this contract as the target:

// src/Bakery.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
 
interface IOracle { function price() external view returns (uint256); }
 
contract Bakery {
    address public owner;
    IOracle public oracle;
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;
    bool public paused;
 
    constructor(address _oracle) {
        owner = msg.sender;
        oracle = IOracle(_oracle);
    }
 
    // BUG 1: missing access control
    function setOracle(address _oracle) external {
        oracle = IOracle(_oracle);
    }
 
    // BUG 2: reentrancy (state update after external call)
    function withdraw() external {
        uint256 amt = balances[msg.sender];
        require(amt > 0);
        (bool ok,) = msg.sender.call{value: amt}("");
        require(ok);
        balances[msg.sender] = 0;
        totalDeposits -= amt;
    }
 
    function deposit() external payable {
        require(!paused);
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }
 
    // BUG 3: weak randomness
    function lottery() external view returns (uint256) {
        return uint256(keccak256(abi.encodePacked(block.timestamp, block.prevrandao))) % 100;
    }
 
    // BUG 4: tx.origin
    function selfDestruct() external {
        require(tx.origin == owner);
        selfdestruct(payable(owner));
    }
 
    // BUG 5: solvency invariant violation possible via overflow-protected but logically-wrong path
    function rebase(int256 delta) external {
        require(msg.sender == owner);
        if (delta > 0) totalDeposits += uint256(delta);
        else totalDeposits -= uint256(-delta);
        // No corresponding update to balances — totalDeposits drifts from sum(balances)
    }
 
    function pause() external {
        require(msg.sender == owner);
        paused = true;
    }
}

Task — run each tool, record what it finds:

# Slither
slither . --json slither.json | tee slither.txt
 
# Aderyn
aderyn . --output aderyn.md
 
# Echidna — property contract
cat > test/echidna/EchidnaBakery.sol <<'EOF'
pragma solidity ^0.8.20;
import "../../src/Bakery.sol";
contract MockOracle { function price() external pure returns (uint256) { return 1e18; } }
contract EchidnaBakery is Bakery {
    constructor() Bakery(address(new MockOracle())) {}
    function echidna_solvent() public view returns (bool) {
        return address(this).balance >= totalDeposits;
    }
    function echidna_lottery_bounded() public view returns (bool) {
        return Bakery(address(this)).lottery() < 100;
    }
}
EOF
echidna test/echidna/EchidnaBakery.sol --contract EchidnaBakery --config echidna.yaml
 
# Foundry invariant (handler in test/invariant/, see §9.4 template)
forge test --match-path test/invariant/*.t.sol -vvv
 
# Halmos
cat > test/halmos/CheckBakery.t.sol <<'EOF'
pragma solidity ^0.8.20;
import "forge-std/Test.sol";
import "../../src/Bakery.sol";
contract MockOracle { function price() external pure returns (uint256) { return 1e18; } }
contract CheckBakery is Test {
    Bakery b;
    function setUp() public { b = new Bakery(address(new MockOracle())); }
    function check_anyone_can_setOracle(address attacker, address newOracle) public {
        vm.assume(attacker != b.owner());
        vm.prank(attacker);
        b.setOracle(newOracle);  // should revert, but doesn't
        assert(address(b.oracle()) != newOracle);  // assertion fails -> bug
    }
}
EOF
halmos --function check_

Produce a comparison table:

Bug	Slither	Aderyn	Echidna	Foundry invariant	Halmos
setOracle no ACL	?	?	only if you fuzz `setOracle`	only via handler	yes (with `check_anyone_can_setOracle`)
withdraw reentrancy	high-confidence	likely	yes (state-violation property)	yes	possible
weak randomness	yes	yes	n/a	n/a	n/a
tx.origin	yes	yes	n/a	n/a	n/a
rebase solvency	no	no	likely (with `echidna_solvent`)	yes (with handler tracking sum(balances))	with explicit property

Write up which tool caught what and why. The point: no tool catches everything. Each finds its specialty; missing tools leaves gaps. The auditor is the integrator.

18.3 Lab 2 — Full mock audit on a stripped ERC-4626 vault

Use the following vault (with two seeded bugs) as the audit target:

// src/MockVault.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
 
import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
import {ERC20}  from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
 
contract MockVault is ERC20 {
    IERC20 public immutable asset;
    address public owner;
 
    constructor(IERC20 _asset) ERC20("MockVault", "mvBT") {
        asset = _asset;
        owner = msg.sender;
    }
 
    function totalAssets() public view returns (uint256) {
        return asset.balanceOf(address(this));
    }
 
    function convertToShares(uint256 assets) public view returns (uint256) {
        uint256 supply = totalSupply();
        if (supply == 0) return assets;
        // BUG A — donation-attack vulnerable; OZ patches this with virtual offset.
        return (assets * supply) / totalAssets();
    }
 
    function convertToAssets(uint256 shares) public view returns (uint256) {
        uint256 supply = totalSupply();
        if (supply == 0) return shares;
        return (shares * totalAssets()) / supply;
    }
 
    function deposit(uint256 assets, address rcv) external returns (uint256 shares) {
        shares = convertToShares(assets);
        require(asset.transferFrom(msg.sender, address(this), assets), "xfer");
        _mint(rcv, shares);
    }
 
    function redeem(uint256 shares, address rcv, address ownerOf) external returns (uint256 assets) {
        if (msg.sender != ownerOf) {
            _spendAllowance(ownerOf, msg.sender, shares);
        }
        assets = convertToAssets(shares);
        _burn(ownerOf, shares);
        require(asset.transfer(rcv, assets), "xfer");
    }
 
    // BUG B — admin can swap asset; no event, no validation, no timelock
    function setAsset(IERC20 newAsset) external {
        require(msg.sender == owner);
        // assembly hack — directly write immutable's storage backing... in real protocols
        // this might be an admin upgrade hook that swaps asset reference
        // for lab: simulate by storing in a regular var
    }
}

(For the lab: in practice, BUG B is encoded as a hidden admin function — the finding is that swapping asset is destructive and unguarded. Replace immutable with a regular IERC20 public asset for the lab to make the bug actually reachable.)

Task — produce three deliverables:

Threat model document (file: audit/threat-model.md) — actors, trust boundaries, STRIDE per Function. ≥ 1 page.
Invariant list (file: audit/invariants.md) — ≥ 8 invariants for the vault, ≥ 4 of them turned into Foundry invariant tests.
Three findings written up (files: audit/findings/F-001-donation-attack.md, F-002-asset-swap-no-timelock.md, F-003-missing-events.md) — full template, severity assigned, PoC for each.

Submit as a Git branch.

18.4 Lab 3 — Write a custom Slither detector

Project-specific anti-pattern: “any function that writes the oracle storage variable must have an onlyOwner modifier”.

Use the template in §8.3. Save to detectors/oracle_setter_acl.py. Run:

slither . --detect oracle-setter-acl --detectors-paths detectors/

Expected: flags Bakery.setOracle (from Lab 1) and any similar function in the vault lab.

Stretch: extend the detector to also flag any function that writes oracle without emitting an event whose first topic is keccak256("OracleSet(address)"). This combines two anti-patterns into one detector.

18.5 Expected outcomes

Tooling bake-off table with explicit notes on which tool caught which bug.
Mock-audit deliverables (threat model, invariants, 3 findings) reviewable by another auditor.
Working custom Slither detector that flags the project-specific anti-pattern.

If you can do these three things, you have produced exactly what a junior auditor at a firm produces in their first month.

19. Anti-patterns (process-level, add to master checklist)

20. Trade-offs and Open Debates

Decision	Option A	Option B	Auditor’s view
Static tool primary	Slither	Aderyn	Run both. They disagree usefully. Slither is more battle-tested; Aderyn is faster startup and Rust-native.
Fuzz engine primary	Echidna	Medusa / Foundry invariant	Foundry for DX, Medusa for deep runs, Echidna as a tiebreaker. Don’t pick one.
Symbolic tool	Halmos	Certora	Halmos for solo work / no budget. Certora for funded engagements where the protocol justifies the cost.
Severity rubric in private audits	Code4rena style	Custom	Code4rena style is familiar to clients and well-documented. Custom rubric is fine only with explicit definitions in the report’s methodology section.
Time allocation	Manual-heavy (60%+)	Tool-heavy (40%+)	Manual-heavy. Tools are cheap; manual is the diff between commodity and senior audit.
Disclosure window	Standard 90 days	Project-by-project	Negotiate up front. Default to industry-standard timelines and put it in the engagement letter.
Re-audit included	Yes (within engagement)	Quoted separately	Include up to a defined window (e.g., 2 weeks after final report). Quote separately if it extends beyond.
Public report after audit	Yes	No	Default: yes after fixes + cooling-off. Clients who refuse public reporting are a yellow flag; sometimes valid (pre-launch IP), often not.

21. Quiz (≥80% to advance)

Q: A client asks for a “quick audit” of a 3000-SLOC novel-math AMM in 3 days. What’s the response? A: Decline or reshape. At ~300 SLOC/day for novel math with complexity multipliers (×1.5 for novel math), the realistic estimate is ~15 auditor-days. Three days yields either incomplete coverage or a low-quality report; both damage the auditor’s reputation. Propose a 2-auditor 8-day plan or refer elsewhere.
Q: You run Slither on a codebase. It flags 20 reentrancy issues. Half look like real reentrancy; half look like false positives because they’re in view functions. How do you proceed? A: Triage each. view functions can still be read-only reentrancy targets if they’re consumed by other protocols as oracles. Don’t dismiss a Slither finding by category; verify each. Open a finding per real issue (often consolidated by root cause); document dismissed false positives in audit notes with reason.
Q: What’s the difference between a property-mode and assertion-mode Echidna test? A: Property mode: write echidna_foo() that returns bool; Echidna fails the test when it returns false. Assertion mode: use Solidity assert(...) inside any function called by the fuzzer; Echidna fails when an assertion trips. Assertion mode is more flexible (mid-function checks); property mode reads cleaner for end-state invariants.
Q: Why is the “handler pattern” essential in Foundry invariant testing? A: Direct-target fuzzing of business contracts produces overwhelmingly reverting calls (invalid inputs, wrong state, etc.), yielding shallow coverage. A handler wraps target functions with bound() and bookkeeping (ghost variables), constraining inputs to valid ranges and tracking cumulative state. This dramatically increases meaningful execution depth.
Q: When is Halmos a better choice than fuzzing? A: When you need exhaustive coverage within a bound (e.g., a pure math function over all 256-bit inputs), or when proving access control (no caller without role X can do Y). Fuzzing samples; symbolic execution explores. Halmos is bounded — large state and unbounded loops force concrete fallbacks.
Q: Under Sherlock’s rubric, a bug causes a 0.5% loss of user fees when a rare market condition holds. Severity? A: Medium. >0.01% AND >$10 thresholds are met; the rare condition makes it Medium-not-High under the “specific conditions” clause. Likelihood is not considered for validity, so the rarity doesn’t invalidate the finding — it just keeps it from being High.
Q: A client wants to downgrade a High to Medium because “an attacker would need to control the keeper”. Your response? A: Check the scoping doc / threat model. If keeper is documented as a privileged role assumed honest, downgrade may be warranted but only with explicit rationale (“Medium because keeper compromise is a documented risk category and the audit’s trust model assumes keeper honesty within bounded conditions”). If keeper trust isn’t documented, the assumption isn’t justified — keep at High and note the missing trust documentation.
Q: You’re 2 days into a 10-day audit and find a Critical bug. The client asks you to disclose and pause. What do you do? A: Immediately. Stop the audit clock. Coordinate immediate disclosure to the client’s security contact. If mainnet-deployed, push for an immediate pause (if pausable) and on-chain incident response. Document the disclosure timeline in the final report. Some auditors include a “critical disclosure clause” in the engagement letter pre-defining this flow.
Q: What’s the one thing a custom Slither detector gives you that a generic detector can’t? A: Project-specific patterns. Generic detectors find “delegatecall to user-controlled address”; custom detectors find “any function writing oracle must have onlyOwner” or “any function calling IERC20.transfer must use SafeERC20”. The investment is small (~30 min); the catch rate on project-specific anti-patterns is high.
Q: A protocol’s “invariant” is “total supply equals sum of user balances”. You write a Foundry invariant test that fails after 256 runs at depth 50. The bug is rounding. The client says “rounding is acceptable, off by 1 wei”. Severity? A: It depends on direction. If the rounding favors the protocol (user loses 1 wei to dust accumulation) and is bounded — typically Low or Q&A. If the rounding favors the user (user can extract more than they deposited via repeated rounding) — Medium or High depending on the per-tx extract rate vs gas cost. Direction matters. Spell it out and provide a worked numeric example for the report.

22. Week 15 Deliverables

Tooling installed and working: Foundry, Slither, Aderyn, Echidna, Medusa, Halmos, Solhint.
Single Foundry repo with Bakery.sol (Lab 1) where each of the five seeded bugs is documented against which tool(s) caught it.
Mock audit on MockVault.sol with three deliverables: threat model doc, invariants list (≥ 8), 3 finding write-ups.
One custom Slither detector written and run successfully against your lab project (oracle-setter-acl or similar).
One Halmos check_* test that proves a specific access-control property symbolically.
Master audit checklist updated with this week’s process-level anti-patterns (§19).
Notes file: written reflection on which tool surprised you most (positive or negative) and why.

23. Where this leads

Next week: Tuan-16-Report-Writing-Capstone. You take the artifacts you produced this week (scoping doc, threat model, invariant list, findings) and learn to package them into a polished audit report at the level of a top-firm deliverable. Then you spend the back half of the week on the capstone: a real 40-hour audit of a multi-module protocol with multiple seeded bugs, produced end-to-end including remediation review.

The arc of the course closes: Weeks 1–4 built EVM and Solidity literacy; Weeks 5–7 built the vulnerability vocabulary; Weeks 8–11 built protocol and economic reasoning; Weeks 12–14 covered adjacent surfaces; Week 15 (this lesson) glued it all into a methodology; Week 16 makes it a deliverable.

After Week 16, the loop is:

Pick a real protocol (Code4rena / Sherlock / Cantina contest, or an open invitation).
Apply the methodology.
Submit findings.
Read judge decisions; calibrate severity judgement against the community.
Iterate weekly.

Auditing is a portfolio profession. The methodology is what makes the portfolio repeatable.

Last updated: 2026-05-16 See also: Roadmap · References · Tuan-04-Security-Foundations-CEI-AC · Tuan-05-Vulnerability-Classes-Part-1 · Tuan-06-Vulnerability-Classes-Part-2 · Tuan-16-Report-Writing-Capstone · Tuan-Bonus-Formal-Verification-Deep · Tuan-Bonus-Fuzzing-Invariant-Advanced

lthieu's notes

Explorer

Tuan-15-Audit-Methodology-Tooling

Week 15 — Audit Methodology & Tooling

1. Context & Why

1.1 What this week is and isn’t

1.2 The mindset shift

1.3 Learning goals

1.4 Primary references

2. The Audit Lifecycle

2.1 The full pipeline

2.2 Time-box discipline

3. Pre-engagement & Scoping

3.1 What goes into a scoping document

3.2 SLOC, complexity, and “audit day” estimation

3.3 Day rate & fees (orientation, not advice)

3.4 NDA, COI, disclosure norms

3.5 Scoping deliverable template

4. Kickoff & Documentation Review

4.1 Documentation as evidence

4.2 The “first 60 minutes” walkthrough

4.3 Setting up your repo

5. Threat Modeling

5.1 STRIDE adapted to Web3

5.2 Per-actor attacker model

5.3 Trust boundaries

5.4 Threat model document template

6. Invariant Identification

6.1 What is an invariant (precisely)

6.2 How to find invariants

6.3 Invariant catalogue by protocol type

AMM (constant-product, e.g., Uniswap V2 fork)

Lending market (Aave / Compound style)

ERC-4626 vault

Bridge / cross-chain

6.4 Invariant catalogue document

7. Manual Review

7.1 Three passes

Pass 1 — Top-down (the user’s path)

Pass 2 — Bottom-up (the state’s path)

Pass 3 — Cross-cutting

7.2 The diff-review (for re-audits)

7.3 Heuristics that fire fast

8. Static Analysis — Slither, Aderyn, and Custom Detectors

8.1 Why static analysis still matters

8.2 Slither — the workhorse

8.3 Custom Slither detectors

8.4 Aderyn (Cyfrin) — Rust alternative

8.5 Solhint — style + light security

8.6 Mythril, Manticore — legacy

8.7 SWC Registry — historical reference

9. Fuzzing — Echidna, Medusa, Foundry Invariant

9.1 Why fuzz

9.2 Echidna

9.3 Medusa

9.4 Foundry invariant testing — handler pattern

9.5 Fuzzer comparison — what each catches

10. Symbolic Execution & Formal Verification

10.1 Halmos — Foundry-compatible symbolic checks

10.2 Certora Prover — heavyweight formal verification

10.3 K framework — for the truly motivated

10.4 When to reach for symbolic/formal

11. Differential & Fork Testing

11.1 Differential testing

11.2 Fork testing — production state as fixture

12. Economic Risk Analysis

12.1 The non-code attack surface

12.2 Modeling

13. Severity Classification

13.1 The three dominant rubrics

13.2 Immunefi V2.3 (smart contract — impact based)

13.3 Code4rena rubric

13.4 Sherlock rubric (strict)

13.5 Defending severity to the client

13.6 Likelihood = capital + access + complexity

14. Tooling Setup — All-in-one Foundry Project

15. Tenderly — Simulation, Debugging, Monitoring

15.1 Use cases

15.2 Audit workflow with Tenderly

15.3 Alternative tooling