Source contract
    ↓
Static analysis layer (Slither, Mythril, Semgrep Solidity)
    ↓
Structured candidate findings (location, pattern, data flow)
    ↓
LLM semantic reasoning (intent, exploitability, context)
    ↓
Vulnerability hypothesis (with confidence + rationale)
    ↓
Cascaded verification (eliminates false positives)
    ↓
Finding output (severity, PoC reference, remediation)

Protocol source + documentation
    ↓
Invariant extraction (LLM + heuristic scaffold)
    ↓   "What must always be true for this protocol to be safe?"
List of candidate invariants
    ↓
Formalization (each invariant → a checkable property)
    ↓   e.g., "balanceOf(vault) >= sum(deposits)" → a runtime assertion or a spec for a prover
Verification (runtime fuzzing, symbolic execution, formal proof)
    ↓
Invariant violations → candidate logic bugs
    ↓
LLM confirmation (is this violation economically exploitable?)
    ↓
Confirmed logic finding

// Foundry exploit PoC — reentrancy on a vulnerable vault
contract Exploit is Test {
    VulnerableVault vault;
    address attacker = makeAddr("attacker");

    function setUp() public {
        // Fork mainnet at a block where the vault is deployed
        vm.createFork(MAINNET_RPC, BLOCK_NUMBER);
        vault = VulnerableVault(VAULT_ADDRESS);
        // Fund attacker
        vm.deal(attacker, 100 ether);
    }

    function test_reentrancy_exploit() public {
        uint256 vaultBalanceBefore = address(vault).balance;
        vm.startPrank(attacker);
        // Attacker deposits, then exploits reentrancy on withdraw
        AttackContract attack = new AttackContract(vault);
        attack.attack{value: 10 ether}();
        vm.stopPrank();
        uint256 vaultBalanceAfter = address(vault).balance;
        // Verification: vault balance decreased, attacker profit > 0
        assertLt(vaultBalanceAfter, vaultBalanceBefore);
        assertGt(attacker.balance, 100 ether);  // started with 100
    }
}

Generated patch
    ↓
Gate 1: Slither/Mythril — original finding gone? no new findings?
    ↓ pass                              ↓ fail → reject patch
Gate 2: Test suite / property tests — all pass?
    ↓ pass                              ↓ fail → reject patch
Gate 3: Exploit PoC re-run — exploit now fails?
    ↓ pass                              ↓ fail → reject patch
Gate 4: Formal verification (if feasible) — property holds?
    ↓ pass                              ↓ fail → reject patch
Verified patch → human approval gate
    ↓
Deployment

# Module S11 — Smart Contract Audit Harnesses

**Course**: 2A — Building AI Harnesses for Cybersecurity
**Module**: S11 — Smart Contract Audit Harnesses
**Duration**: 90 minutes
**Level**: Senior Engineer and above
**Prerequisites**: S00–S10 complete; Pillars 1–3 established the harness architecture, scope enforcement, evidence chain, and triage patterns this module specializes to the EVM.

> *Three modes — Detect, Patch, Exploit — benchmarked against EVMbench's 117 vulnerabilities across 40 repositories. Static analysis finds patterns; the LLM reasons about intent; cascaded verification eliminates false positives. Heimdallr anchors the design at $2.31 per 10K LOC and 92.45% detection.*

---

## Learning Objectives

1. Design the three-mode EVM audit architecture (Detect, Patch, Exploit) and defend why LLMs alone fail on smart contract code.
2. Build an invariant extraction and checking harness for business-logic vulnerabilities, including flash loan attack paths that span multiple contracts.
3. Construct a Foundry-based proof-of-concept exploit on forked mainnet and capture structured evidence (transaction hash, state delta, economic impact).
4. Implement a patch generation pipeline with cascaded verification quality gates and a human approval gate.
5. Map the harness to EVMbench's taxonomy and Heimdallr's cost model, and explain the 92% vs 34% gap between purpose-built agents and general LLMs on DeFi.

---

# S11.1 — The EVM Audit Architecture

A smart contract security harness is not a single scanner. It is a three-mode system: **Detect** (find vulnerabilities), **Patch** (generate fixes), **Exploit** (build and run proof-of-concept attacks). EVMbench — the benchmark from OpenAI and Paradigm — evaluates agents across exactly these three modes on 117 curated vulnerabilities drawn from 40 real EVM repositories. A harness that only detects is half a harness; the benchmark demands all three.

## Why LLMs alone fail on smart contracts

The tempting shortcut is to point a frontier LLM at a Solidity file and ask "find the bugs." This fails for three structural reasons:

1. **Hallucinations on Solidity semantics.** The EVM has precise, counter-intuitive semantics — integer overflow wraps at 2^256, `transfer()` forwards 2300 gas, `address(this).balance` reads the contract's ether not an accounting variable. An LLM trained mostly on Python and JavaScript will confidently assert behavior that is wrong at the opcode level. The hallucination is not random noise; it is systematic, because the model applies general-language intuitions to a domain where those intuitions mislead.

2. **Context limits on large codebases.** A DeFi protocol is not one contract. It is a constellation — the core vault, the router, the oracle, the governance token, the staking wrapper, and their inherited base contracts. A serious protocol audit reads 5,000 to 50,000 lines of Solidity across dozens of files. No context window holds that with the precision a security audit demands, and compaction silently drops the storage variable declared 40 files away that makes the flash loan path exploitable.

3. **False positives on benign patterns.** Reentrancy detection is the canonical example. The checks-effects-interactions pattern is safe; a naive LLM flags any external call as a reentrancy risk. On a real codebase, an LLM-only pass produces dozens of false positives that a human auditor must then refute — the harness becomes a cost center, not a force multiplier.

## The harness pipeline: static analysis feeds the LLM

The architecture that works pairs static analysis with LLM semantic reasoning. The static tools do what they are good at — taint tracking, pattern matching, control-flow graph construction — and produce structured candidate findings. The LLM does what it is good at — reasoning about intent, reading the economic logic, judging whether a candidate is real in context. The LLM never starts from raw source; it starts from static-analysis candidates plus their location, data flow, and severity hints.

```text
Source contract
    ↓
Static analysis layer (Slither, Mythril, Semgrep Solidity)
    ↓
Structured candidate findings (location, pattern, data flow)
    ↓
LLM semantic reasoning (intent, exploitability, context)
    ↓
Vulnerability hypothesis (with confidence + rationale)
    ↓
Cascaded verification (eliminates false positives)
    ↓
Finding output (severity, PoC reference, remediation)
```

Slither (Trail of Bits) does taint analysis and detects 90+ vulnerability patterns via its detector set. Mythril performs symbolic execution to find execution paths that violate safety properties. Semgrep Solidity adds custom rule-based pattern matching. None of these is sufficient alone — Slither is fast but pattern-limited, Mythril is thorough but slow and noise-prone on large code. The harness runs all of them, deduplicates candidates, and routes the survivors to the LLM.

## Heimdallr's architecture: the anchor design

Heimdallr (arXiv 2601.17833) is the anchor system for this module. It achieved a **92.45% detection rate** at a cost of **$2.31 per 10,000 lines of code** in contest-style auditing, and reconstructed **17 of 20 real-world attacks** that occurred after June 2025. Three innovations matter for harness design:

1. **Function-level code reorganization.** Rather than feeding the LLM an entire contract (which overflows context or forces lossy compaction), Heimdallr reorganizes the code into function-level units and feeds the model the relevant functions plus their call graph context. The model sees the function under analysis, the functions it calls, and the storage variables it touches — and nothing else. This minimizes context overhead while preserving the information needed for semantic reasoning.

2. **Heuristic reasoning for business logic.** For business-logic vulnerabilities (S11.2), Heimdallr uses a heuristic layer that encodes domain knowledge — "does this function check the caller's balance before transferring?", "is the price oracle manipulable in a single transaction?", "does the protocol assume the token balance equals the accounting variable?". These heuristics give the LLM a scaffold to reason about intent, which raw pattern matching cannot.

3. **Cascaded verification to eliminate false positives.** Every LLM-produced hypothesis passes through a verification cascade: static analysis re-checks the claim, the test suite is run against the hypothesized vulnerability, and formal verification is applied where the property is expressible. A finding is output only if it survives the cascade. This is what drives the high precision — false positives are filtered before they reach the auditor.

## The three modes as a coherent system

The three modes are not three separate harnesses. They share the static-analysis layer, the code reorganization, and the engagement memory (the structured record of contracts scanned, candidates found, hypotheses verified). Detect produces findings; Exploit turns confirmed findings into runnable PoCs; Patch produces fixes that are themselves verified against the exploit (the patch must make the PoC fail). The modes feed each other — a confirmed exploit is the strongest possible evidence for a detection finding, and a patch that does not break the exploit is not a patch.

---

# S11.2 — Business Logic Vulnerability Detection

Business-logic vulnerabilities are the hardest class in smart contract security. A reentrancy or integer overflow has a recognizable syntactic signature — an external call in a state-changing function, an unchecked arithmetic operation. A business-logic bug has no such signature. The code is syntactically valid, passes every static check, and is economically exploitable. The 2022 Beanstalk governance attack ($182M) exploited a logic flaw: the protocol allowed governance proposals to execute arbitrary code, and a flash-loan-funded proposal drained the protocol in a single transaction. No static analyzer flags that.

## Why static analysis cannot check intent

Static analysis checks patterns against a catalog of known-bad patterns. It can find "external call before state update" (reentrancy) or "unchecked subtraction" (underflow). It cannot find "this function assumes the oracle price is honest, but the oracle is manipulable in a single block" because that is not a pattern — it is a property of the protocol's economic design. The bug is not in any single line; it is in the relationship between the code and the protocol's intended invariants.

The harness strategy is **invariant extraction**: identify what the protocol intends to be always-true, then check whether the code enforces it. An invariant is a property that must hold across all reachable states — "the sum of user deposits equals the contract's token balance", "a governance proposal cannot execute in the same transaction it is created", "the oracle price is taken from a time-weighted average over at least N blocks". When the harness finds a state where an invariant can be violated, it has found a logic bug.

## The invariant extraction pipeline

```text
Protocol source + documentation
    ↓
Invariant extraction (LLM + heuristic scaffold)
    ↓   "What must always be true for this protocol to be safe?"
List of candidate invariants
    ↓
Formalization (each invariant → a checkable property)
    ↓   e.g., "balanceOf(vault) >= sum(deposits)" → a runtime assertion or a spec for a prover
Verification (runtime fuzzing, symbolic execution, formal proof)
    ↓
Invariant violations → candidate logic bugs
    ↓
LLM confirmation (is this violation economically exploitable?)
    ↓
Confirmed logic finding
```

The LLM's role is twofold. First, it extracts candidate invariants by reading the code and documentation — the protocol's own docs often state the intended invariants in plain language, and the code's comments frequently assert them. Second, it confirms whether a detected violation is exploitable: a violation that requires an attacker to already own 51% of the token supply is theoretical; a violation reachable via a flash loan in a single transaction is critical.

## Context budget management for large contracts

Heimdallr's function-level reorganization (S11.1) is the solution to the context problem for logic bugs specifically. A DeFi vault contract may be 2,000 lines, but the function that handles withdrawals is 80 lines. The harness feeds the LLM that function, the storage variables it reads and writes, and the external functions it calls — and asks "what invariants must hold for this function to be safe?". The model reasons about a tractable slice of the protocol, not the entire monolith.

For cross-contract logic — the flash loan case — the harness extends the context window along the call graph. If `Vault.withdraw()` calls `Oracle.getPrice()`, and `Oracle.getPrice()` reads from a spot DEX pool, the harness includes all three in the LLM's context, along with the data-flow edges between them. The model can then reason: "the withdrawal amount is computed from `Oracle.getPrice()`, which reads a spot price; a flash loan can manipulate that spot price in the same transaction; therefore the withdrawal can be inflated." That is a flash loan attack path, identified by reasoning over the call graph, not by pattern matching.

## Flash loan attack paths

A flash loan lets a borrower borrow any amount with no collateral, provided the loan is repaid in the same transaction. This collapses the constraint that an attacker needs capital — they can act as a whale for the duration of one transaction. Any protocol whose safety depends on "an attacker cannot afford to manipulate the market" is vulnerable if a flash loan can substitute for capital.

The harness detects flash loan paths by tracing data flow from external price/oracle sources through to state-changing operations, and checking whether the price source is manipulable in a single transaction. Spot DEX prices are manipulable; time-weighted average prices (TWAP) over multiple blocks are not (or are harder). The harness flags any protocol that consumes a spot price in a way that affects value transfer.

---

# S11.3 — Exploit Chain Construction

Detection without exploitation is a hypothesis. A finding that says "this contract is vulnerable to reentrancy" is a claim; a finding that includes a transaction hash showing the reentrancy executed and drained funds is evidence. EVMbench's Exploit mode scores agents on whether they can write and run a working exploit, not merely identify the vulnerability. This is the standard the harness meets.

## PoC structure: setup, attack, verification

A proof-of-concept exploit has three phases:

1. **Setup.** Deploy or fork the target contract into a test environment. Fund the attacker account. Set up any prerequisites — a malicious token contract, a flash loan provider, a fake oracle. The setup must reproduce the on-chain conditions under which the vulnerability exists.

2. **Attack transaction.** Execute the exploit. For reentrancy, this is the malicious contract that re-enters the vulnerable function. For a flash loan attack, this is the borrow → manipulate → exploit → repay sequence in a single transaction. For a governance attack, this is the proposal + flash-loan-funded vote + execution.

3. **Verification.** Assert that the exploit succeeded. Check the attacker's balance increased. Check the protocol's balance decreased. Calculate the economic impact — the dollar value at the exploit's exchange rate. If the assertion fails, the exploit did not work, and the finding is downgraded or retracted.

```solidity
// Foundry exploit PoC — reentrancy on a vulnerable vault
contract Exploit is Test {
    VulnerableVault vault;
    address attacker = makeAddr("attacker");

    function setUp() public {
        // Fork mainnet at a block where the vault is deployed
        vm.createFork(MAINNET_RPC, BLOCK_NUMBER);
        vault = VulnerableVault(VAULT_ADDRESS);
        // Fund attacker
        vm.deal(attacker, 100 ether);
    }

    function test_reentrancy_exploit() public {
        uint256 vaultBalanceBefore = address(vault).balance;
        vm.startPrank(attacker);
        // Attacker deposits, then exploits reentrancy on withdraw
        AttackContract attack = new AttackContract(vault);
        attack.attack{value: 10 ether}();
        vm.stopPrank();
        uint256 vaultBalanceAfter = address(vault).balance;
        // Verification: vault balance decreased, attacker profit > 0
        assertLt(vaultBalanceAfter, vaultBalanceBefore);
        assertGt(attacker.balance, 100 ether);  // started with 100
    }
}
```

## Foundry and Hardhat on forked mainnet

The harness runs PoCs against a forked mainnet environment, not a clean local chain. A forked mainnet reproduces the target contract's actual storage, the real token contracts it integrates with, and the actual oracle prices at the forked block. This matters because many exploits depend on the precise state of the blockchain — the liquidity in a DEX pool, the governance proposal queue, the oracle's last reported price.

Foundry (with `forge test --fork-url`) is the primary tool. It is fast, supports Solidity-native test writing, and integrates cleanly with CI. Hardhat is the alternative for teams with a JavaScript/TypeScript toolchain. The harness wraps either as a tool: input is the PoC Solidity file and fork configuration, output is the test result (pass/fail), the transaction trace, the state delta, and the gas used.

## Evidence collection for exploit findings

An exploit finding's evidence is structured, not narrative:

| Field | Content |
| --- | --- |
| **Transaction hash** | The hash of the exploit transaction in the forked environment |
| **Block number** | The forked block — the state at which the exploit is valid |
| **State before** | Relevant storage slots and balances before the attack |
| **State after** | Relevant storage slots and balances after |
| **Call trace** | The sequence of internal and external calls in the exploit |
| **Economic impact** | Token amounts and dollar value at the fork block's prices |
| **PoC file** | The Solidity/TypeScript PoC, reproducible with `forge test` |

This structured evidence is what makes the finding actionable. A client who receives "reentrancy in `Vault.withdraw()`" can argue it is theoretical. A client who receives a transaction trace showing 10,000 ETH moved from the vault to the attacker account in a forked-mainnet PoC cannot.

---

# S11.4 — Patch Generation and Cascaded Verification

Generating a fix is harder than finding the bug. The patch must remove the vulnerability while preserving every intended behavior the contract provides. A patch that "fixes" reentrancy by removing the withdraw function fixes the bug and breaks the protocol. Heimdallr's cascaded verification is the quality-control mechanism that distinguishes a real patch from a breakage.

## The cascaded verification layer

Every generated patch passes through a cascade of checks:

1. **Static analysis re-check.** Run Slither (and Mythril where feasible) on the patched code. The original finding must be gone. No new findings should appear. A patch that closes a reentrancy but introduces an integer overflow has failed.

2. **Test suite.** The protocol's existing test suite must pass. If the protocol has no test suite (common for early-stage projects), the harness generates property tests from the invariants extracted in S11.2 and runs those. A patch that breaks a passing test has failed — it changed behavior, not just security.

3. **Exploit re-run.** The PoC from S11.3 must now fail. If the exploit still drains the vault, the patch did not address the actual attack path. This is the strongest check — it directly verifies that the specific exploit the harness constructed no longer works.

4. **Formal verification (where feasible).** For properties expressible as formal specs — "the sum of deposits is always >= the contract balance", "only the owner can call `setAdmin`" — run a prover (e.g., Certora, Halmos) on the patched code. Formal verification is not always feasible (complex economic properties resist formalization), but when it is, it provides the strongest guarantee.

```text
Generated patch
    ↓
Gate 1: Slither/Mythril — original finding gone? no new findings?
    ↓ pass                              ↓ fail → reject patch
Gate 2: Test suite / property tests — all pass?
    ↓ pass                              ↓ fail → reject patch
Gate 3: Exploit PoC re-run — exploit now fails?
    ↓ pass                              ↓ fail → reject patch
Gate 4: Formal verification (if feasible) — property holds?
    ↓ pass                              ↓ fail → reject patch
Verified patch → human approval gate
    ↓
Deployment
```

## Patch quality gates

The four gates are not optional. A patch that fails any gate is rejected and the harness either regenerates (with the failure as feedback) or escalates to the human auditor. The gates encode the definition of a correct patch: the bug is gone, nothing broke, the exploit fails, and (where checkable) the property holds.

The gates also catch a class of patch failure that is easy to miss: the patch that fixes the specific PoC but not the underlying vulnerability. If the harness's PoC used a 10 ETH deposit, and the patch adds a check that deposits must be exactly 10 ETH, the PoC fails but the vulnerability remains — a 50 ETH deposit still exploits it. The static-analysis and formal-verification gates catch this; the exploit re-run alone would not.

## The approval gate: human in the loop

The harness generates patches; a human auditor approves them. This is non-negotiable. Smart contracts are immutable once deployed (upgradeable proxies aside), and a buggy patch deployed to mainnet can cause losses that cannot be reversed. The human approval gate is the last line of defense against a patch that passes all automated gates but is nonetheless wrong — because the gates check what is automatable, and some properties (does this patch change the protocol's economic behavior in a way the team intends?) require human judgment.

The approval gate's workflow: harness produces a verified patch with a diff, a rationale, the gate results, and the original finding. The auditor reviews the diff, confirms the rationale, and either approves (the patch proceeds to deployment) or rejects (with feedback that feeds back into patch regeneration). The harness does not deploy.

---

## Anti-Patterns

### The LLM-only audit

Pointing a frontier LLM at a Solidity file and asking it to find bugs. Hallucinations on EVM semantics, context overflow on real codebases, false positives on benign external calls. Cure: the static-plus-LLM pipeline (S11.1). Static analysis produces structured candidates; the LLM reasons about them.

### Detection without exploitation

A finding report that says "reentrancy in `Vault.withdraw()`" with no PoC. The client cannot assess severity, and the finding may be theoretical. Cure: the Exploit mode (S11.3). Every confirmed finding gets a runnable PoC with structured evidence.

### The patch that breaks the protocol

A fix that closes the vulnerability but changes the contract's intended behavior — removing the withdraw function to fix reentrancy, or adding a check that rejects legitimate transactions. Cure: the cascaded verification gates (S11.4). The test suite and property tests catch behavior changes.

### The patch that fixes the PoC, not the bug

A fix that addresses the specific exploit the harness constructed but leaves the underlying vulnerability intact. Cure: static-analysis re-check and formal verification, not just exploit re-run. The exploit re-run alone is insufficient.

---

## Key Terms

| Term | Definition |
| --- | --- |
| **Three-mode harness** | Detect (find), Patch (fix), Exploit (PoC) — EVMbench's evaluation frame |
| **EVMbench** | Benchmark: 117 curated vulnerabilities across 40 EVM repositories, scored on Detect/Patch/Exploit |
| **Heimdallr** | Anchor audit agent — function-level reorganization, heuristic reasoning, cascaded verification; 92.45% detection at $2.31/10K LOC |
| **Cascaded verification** | Static analysis → test suite → exploit re-run → formal verification; eliminates false positives and validates patches |
| **Invariant extraction** | Identify what the protocol intends to be always-true, then check whether the code enforces it |
| **Flash loan path** | A data-flow path from a manipulable price source to a value transfer, exploitable in a single transaction |
| **Forked mainnet PoC** | An exploit run against a mainnet fork, reproducing the on-chain state at which the vulnerability exists |
| **Approval gate** | Human auditor reviews and approves every generated patch before deployment |

---

## Lab Exercise

See `07-lab-spec.md`. Four labs, all against Damn Vulnerable DeFi: (1) Slither + LLM triage with precision measurement; (2) invariant extraction and checking harness; (3) Foundry exploit PoC on forked mainnet; (4) patch generation with cascaded verification gates.

---

## References

1. **EVMbench** (arXiv 2603.04915) — OpenAI/Paradigm. The benchmark for Detect, Patch, and Exploit modes across 117 vulnerabilities from 40 EVM repos.
2. **Heimdallr** (arXiv 2601.17833) — function-level reorganization, heuristic reasoning, cascaded verification; 92.45% detection at $2.31/10K LOC; 17/20 real-world attack reconstructions.
3. **Slither** (Trail of Bits) — static analysis, taint tracking, 90+ detectors.
4. **Mythril** — symbolic execution for EVM bytecode.
5. **Foundry / Forge** — forked-mainnet exploit PoC execution.
6. **Damn Vulnerable DeFi** — the lab target for all four labs.
7. **S02.2** — the tool-wrapping pattern (this module specializes it to Solidity tools).
8. **S02.3** — the evidence chain (this module structures exploit evidence).
9. **S12** — benchmarking against EVMbench, Solana/cross-chain, audit-as-deliverable.