Diagrams — Module S11: Smart Contract Audit Harnesses

All Mermaid validated in Mermaid Live Editor. n8n JSON is structurally valid and importable.

Diagram 1 — The Three-Mode EVM Audit Harness (n8n)

Type: n8n workflow (importable JSON) Purpose: The primary visual — the full smart contract audit harness as a node graph. Shows the three modes (Detect, Patch, Exploit) sharing the static-analysis layer, code reorganization, and engagement memory.

{
  "name": "S11 — Smart Contract Audit Harness",
  "nodes": [
    { "name": "Contract Ingest", "type": "n8n-nodes-base.manualTrigger", "position": [200, 300], "notes": "Load Solidity source + dependencies into the harness" },
    { "name": "Code Reorganization", "type": "n8n-nodes-base.set", "position": [420, 300], "notes": "Heimdallr function-level reorganization: split to function units + call graph context" },
    { "name": "Static Analysis (Slither/Mythril/Semgrep)", "type": "n8n-nodes-base.executeCommand", "position": [640, 200], "notes": "Taint tracking, pattern detection, symbolic execution → structured candidates" },
    { "name": "Engagement Memory", "type": "n8n-nodes-base.set", "position": [640, 400], "notes": "Contracts scanned, candidates found, hypotheses verified, exploits built" },
    { "name": "LLM Semantic Reasoning", "type": "n8n-nodes-base.set", "position": [860, 300], "notes": "Intent + exploitability judgment on candidates. Heuristic scaffold for business logic." },
    { "name": "Vulnerability Hypothesis", "type": "n8n-nodes-base.set", "position": [1080, 300], "notes": "Candidate finding with confidence + rationale" },
    { "name": "Cascaded Verification", "type": "n8n-nodes-base.set", "position": [1300, 300], "notes": "Static re-check → test suite → exploit re-run → formal proof. Eliminates FPs." },
    { "name": "DETECT: Finding Output", "type": "n8n-nodes-base.set", "position": [1520, 180], "notes": "Severity, location, rationale, PoC reference, remediation hint" },
    { "name": "EXPLOIT: Foundry PoC", "type": "n8n-nodes-base.executeCommand", "position": [1520, 300], "notes": "forked mainnet: setup → attack tx → verify. tx hash, state delta, $ impact" },
    { "name": "PATCH: Generate Fix", "type": "n8n-nodes-base.set", "position": [1520, 420], "notes": "LLM generates diff → gates: Slither clean, tests pass, PoC fails, formal holds" },
    { "name": "Human Approval Gate", "type": "n8n-nodes-base.set", "position": [1740, 420], "notes": "Auditor reviews verified patch. Harness does NOT deploy." }
  ],
  "connections": {
    "Contract Ingest": { "main": [[{ "node": "Code Reorganization", "type": "main", "index": 0 }]] },
    "Code Reorganization": { "main": [[{ "node": "Static Analysis (Slither/Mythril/Semgrep)", "type": "main", "index": 0 }], [{ "node": "Engagement Memory", "type": "main", "index": 0 }]] },
    "Static Analysis (Slither/Mythril/Semgrep)": { "main": [[{ "node": "LLM Semantic Reasoning", "type": "main", "index": 0 }]] },
    "Engagement Memory": { "main": [[{ "node": "LLM Semantic Reasoning", "type": "main", "index": 0 }]] },
    "LLM Semantic Reasoning": { "main": [[{ "node": "Vulnerability Hypothesis", "type": "main", "index": 0 }]] },
    "Vulnerability Hypothesis": { "main": [[{ "node": "Cascaded Verification", "type": "main", "index": 0 }]] },
    "Cascaded Verification": { "main": [[{ "node": "DETECT: Finding Output", "type": "main", "index": 0 }], [{ "node": "EXPLOIT: Foundry PoC", "type": "main", "index": 0 }], [{ "node": "PATCH: Generate Fix", "type": "main", "index": 0 }]] },
    "PATCH: Generate Fix": { "main": [[{ "node": "Human Approval Gate", "type": "main", "index": 0 }]] }
  }
}

Reading the diagram: Left to right. Source contracts are reorganized into function-level units (Heimdallr's innovation) and fed to the static-analysis layer. Static tools produce structured candidates; the LLM reasons about them with a heuristic scaffold for business logic. Hypotheses pass through cascaded verification, which eliminates false positives. Verified findings branch into three modes: Detect produces the finding report, Exploit builds a Foundry PoC on forked mainnet, Patch generates a fix that must survive the verification gates and a human approval gate. Engagement memory persists across all modes.

Diagram 2 — Why LLMs Alone Fail: The Static-Plus-LLM Pipeline

Type: Mermaid (flowchart) Purpose: Shows the three failure modes of LLM-only auditing and how pairing with static analysis fixes each.

flowchart TD
    SRC["Solidity source<br/>(5K–50K LOC, dozens of files)"]

    subgraph FAIL["LLM-only path — three failure modes"]
        direction TB
        HALL["Hallucination on EVM semantics<br/>(overflow wraps at 2^256, transfer = 2300 gas)"]
        CTX["Context overflow on large codebases<br/>(compaction drops the storage var 40 files away)"]
        FP["False positives on benign patterns<br/>(flags every external call as reentrancy)"]
    end

    subgraph FIX["Harness path — static + LLM"]
        direction TB
        SLITHER["Slither: taint tracking, 90+ detectors"]
        MYTH["Mythril: symbolic execution"]
        SEMG["Semgrep: custom Solidity rules"]
        DEDUP["Dedup candidates → structured list"]
        LLM["LLM: intent + exploitability<br/>in context, NOT from raw source"]
        VERIFIED["Verified hypothesis"]
    end

    SRC -->|"naive: feed raw to LLM"| FAIL
    SRC -->|"harness: static first"| SLITHER
    SRC --> MYTH
    SRC --> SEMG
    SLITHER --> DEDUP
    MYTH --> DEDUP
    SEMG --> DEDUP
    DEDUP --> LLM --> VERIFIED

    style FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080
    style FIX fill:#0d1b2a,stroke:#1b4f72,color:#e4e4e8
    style LLM fill:#14141f,stroke:#5eead4,color:#5eead4
    style VERIFIED fill:#0d2818,stroke:#1e8449,color:#82e0aa

Reading the diagram: The left path (LLM-only) hits three structural failures — semantic hallucination, context overflow, false-positive flooding. The right path (harness) runs static analysis first: Slither for taint and patterns, Mythril for symbolic execution, Semgrep for custom rules. Candidates are deduplicated and routed to the LLM, which reasons about intent and exploitability starting from structured candidates (not raw source). The LLM's job changes from "find the bug" (hard, hallucination-prone) to "is this candidate real and exploitable in context" (tractable, verifiable).

Diagram 3 — Invariant Extraction for Business-Logic Bugs

Type: Mermaid (flowchart) Purpose: The business-logic detection strategy — extract intended invariants, check whether code enforces them, identify exploitable gaps. Static analysis alone cannot do this because it checks patterns, not intent.

flowchart TD
    SRC["Protocol source<br/>+ documentation/comments"]
    EXTRACT["Invariant extraction<br/>(LLM + heuristic scaffold)"]
    INV["Candidate invariants:<br/>'deposits sum == vault balance'<br/>'governance proposal cannot execute same-tx'<br/>'oracle price is TWAP over N blocks'"]
    FORMAL["Formalize each invariant<br/>→ runtime assertion or prover spec"]
    VERIFY["Verify:<br/>runtime fuzzing · symbolic exec · formal proof"]
    VIOL["Invariant violation found"]
    CONFIRM["LLM confirmation:<br/>is this economically exploitable?<br/>(flash-loan reachable = critical)"]
    FINDING["Confirmed logic finding"]

    SRC --> EXTRACT --> INV --> FORMAL --> VERIFY
    VERIFY -->|"violation"| VIOL --> CONFIRM
    CONFIRM -->|"exploitable"| FINDING
    CONFIRM -->|"theoretical only"| DEGRADE["Downgrade / log"]

    STATIC["Static analysis<br/>(Slither/Mythril)"]
    STATIC -.->|"checks patterns,<br/>NOT intent"| MISS["Cannot find logic bugs<br/>(Beanstalk governance, oracle manipulation)"]

    style EXTRACT fill:#14141f,stroke:#5eead4,color:#5eead4
    style CONFIRM fill:#14141f,stroke:#5eead4,color:#5eead4
    style FINDING fill:#0d2818,stroke:#1e8449,color:#82e0aa
    style MISS fill:#2a0d0d,stroke:#a00000,color:#f08080
    style DEGRADE fill:#2a1810,stroke:#a04000,color:#f0a868

Reading the diagram: The harness reads the protocol source plus its documentation and comments (which often state intended invariants in plain language). The LLM, scaffolded by domain heuristics, extracts candidate invariants. Each is formalized into a checkable property — a runtime assertion, a fuzz target, or a formal spec. Verification runs fuzzing, symbolic execution, or formal proof. When a violation is found, the LLM confirms whether it is economically exploitable: a violation reachable via flash loan in one transaction is critical; a violation requiring 51% token ownership is theoretical. The lower path shows why static analysis alone misses logic bugs — it checks patterns, not the relationship between code and intent.

Diagram 4 — The Exploit Chain PoC Structure

Type: Mermaid (flowchart) Purpose: The three-phase structure of a proof-of-concept exploit on forked mainnet, and the structured evidence it produces.

flowchart LR
    subgraph SETUP["1. Setup"]
        FORK["Fork mainnet<br/>at block N"]
        FUND["Fund attacker account"]
        DEPS["Deploy prerequisites<br/>(malicious token, fake oracle)"]
    end

    subgraph ATTACK["2. Attack transaction"]
        CALL["Execute exploit<br/>(reentrancy / flash loan / governance)"]
    end

    subgraph VERIFY["3. Verification"]
        ASSERT["Assert: attacker balance up"]
        ASSERT2["Assert: protocol balance down"]
        IMPACT["Calculate $ impact<br/>at fork-block prices"]
    end

    subgraph EVIDENCE["Structured evidence"]
        TX["tx hash"]
        STATE["state before/after"]
        TRACE["call trace"]
        DOLLARS["economic impact"]
        POC["PoC file (reproducible)"]
    end

    SETUP --> ATTACK --> VERIFY --> EVIDENCE

    style SETUP fill:#0d1b2a,stroke:#1b4f72,color:#e4e4e8
    style ATTACK fill:#2a0d0d,stroke:#a00000,color:#f08080
    style VERIFY fill:#0d2818,stroke:#1e8449,color:#82e0aa
    style EVIDENCE fill:#14141f,stroke:#5eead4,color:#5eead4

Reading the diagram: A PoC exploit has three phases. Setup forks mainnet at a specific block (reproducing the on-chain state under which the vulnerability exists), funds the attacker, and deploys any prerequisite contracts. The attack transaction executes the exploit — a reentrancy callback, a flash-loan borrow-manipulate-repay sequence, a governance proposal + vote + execute. Verification asserts the exploit succeeded and calculates the dollar impact. The output is structured evidence: transaction hash, state before and after, the full call trace, the economic impact in token amounts and dollars, and the reproducible PoC file. This evidence is what makes the finding undeniable — a client can run forge test and see the vault drain.

Diagram 5 — Cascaded Verification for Patch Quality

Type: Mermaid (flowchart) Purpose: The four-gate cascade that a generated patch must survive. A patch that fails any gate is rejected or regenerated. The cascade is what makes the patch trustworthy.

flowchart TD
    PATCH["Generated patch<br/>(LLM-produced diff)"]

    G1{"Gate 1: Static re-check<br/>Slither/Mythril on patched code"}
    G1PASS["Original finding gone?<br/>No new findings?"]
    G1FAIL["REJECT — patch incomplete<br/>or introduces new issue"]

    G2{"Gate 2: Test suite<br/>+ property tests"}
    G2PASS["All tests pass?"]
    G2FAIL["REJECT — patch breaks<br/>intended behavior"]

    G3{"Gate 3: Exploit re-run<br/>PoC against patched code"}
    G3PASS["Exploit now fails?"]
    G3FAIL["REJECT — patch does not<br/>address actual attack path"]

    G4{"Gate 4: Formal verification<br/>(if feasible)"}
    G4PASS["Property holds?"]
    G4FAIL["REJECT — formal property<br/>violated"]

    APPROVED["Verified patch<br/>→ human approval gate"]
    HUMAN["Auditor reviews diff,<br/>rationale, gate results"]
    DEPLOY["Approved → deployment<br/>(harness does NOT deploy)"]

    PATCH --> G1
    G1 --> G1PASS
    G1PASS -->|"yes"| G2
    G1PASS -->|"no"| G1FAIL
    G2 --> G2PASS
    G2PASS -->|"yes"| G3
    G2PASS -->|"no"| G2FAIL
    G3 --> G3PASS
    G3PASS -->|"yes"| G4
    G3PASS -->|"no"| G3FAIL
    G4 --> G4PASS
    G4PASS -->|"yes / N/A"| APPROVED
    G4PASS -->|"no"| G4FAIL
    APPROVED --> HUMAN --> DEPLOY

    style PATCH fill:#14141f,stroke:#5eead4,color:#5eead4
    style G1FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080
    style G2FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080
    style G3FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080
    style G4FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080
    style APPROVED fill:#0d2818,stroke:#1e8449,color:#82e0aa
    style DEPLOY fill:#0d2818,stroke:#1e8449,color:#82e0aa
    style HUMAN fill:#2a1810,stroke:#a04000,color:#f0a868

Reading the diagram: A generated patch enters at the top and must pass four gates in sequence. Gate 1: static analysis on the patched code confirms the original finding is gone and no new findings appeared. Gate 2: the protocol's test suite (or harness-generated property tests from S11.2 invariants) all pass — the patch did not change behavior. Gate 3: the exploit PoC from S11.3 is re-run against the patched code and must now fail — the specific attack no longer works. Gate 4: where the property is formally expressible, a prover confirms the invariant holds. A patch that survives all four gates is verified but still requires human approval before deployment. The human gate catches what automation cannot — changes to economic behavior that require the team's judgment.

Diagram 6 — EVMbench Taxonomy and the Three Modes

Type: Mermaid (flowchart) Purpose: Maps EVMbench's 117 vulnerabilities across 5 classes to the three evaluation modes, showing how Detect/Patch/Exploit are scored independently.

flowchart TD
    BENCH["EVMbench<br/>117 vulnerabilities · 40 repositories"]

    subgraph CLASSES["Vulnerability classes"]
        REENT["Reentrancy"]
        INT["Integer overflow/underflow"]
        ACCESS["Access control"]
        FLASH["Flash loan / oracle"]
        LOGIC["Business logic"]
    end

    subgraph MODES["Three evaluation modes"]
        DETECT["DETECT mode<br/>recall: of 117, how many found?"]
        PATCH["PATCH mode<br/>quality: fix removes bug, preserves behavior?"]
        EXPLOIT["EXPLOIT mode<br/>success: working PoC runs on fork?"]
    end

    BENCH --> CLASSES
    CLASSES --> MODES

    HEIM["Heimdallr anchor:<br/>92.45% detection · $2.31/10K LOC<br/>17/20 real-world attacks reconstructed"]
    HEIM -.->|"the bar"| MODES

    style BENCH fill:#14141f,stroke:#5eead4,color:#5eead4
    style DETECT fill:#0d2818,stroke:#1e8449,color:#82e0aa
    style PATCH fill:#0d2818,stroke:#1e8449,color:#82e0aa
    style EXPLOIT fill:#0d2818,stroke:#1e8449,color:#82e0aa
    style HEIM fill:#2a1810,stroke:#a04000,color:#f0a868

Reading the diagram: EVMbench's 117 vulnerabilities span five classes — reentrancy, integer overflow, access control, flash loan/oracle, and business logic. Each vulnerability is scored independently across three modes: Detect (did the agent find it?), Patch (did the fix work without breaking behavior?), Exploit (did the agent build a working PoC?). A harness can score well on Detect and poorly on Exploit — finding bugs is easier than exploiting them. Heimdallr's 92.45% detection rate at $2.31 per 10K LOC is the bar the harness is measured against. The next module (S12) covers running against this benchmark in detail.

# Diagrams — Module S11: Smart Contract Audit Harnesses > All Mermaid validated in Mermaid Live Editor. n8n JSON is structurally valid and importable. --- ## Diagram 1 — The Three-Mode EVM Audit Harness (n8n) **Type**: n8n workflow (importable JSON) **Purpose**: The primary visual — the full smart contract audit harness as a node graph. Shows the three modes (Detect, Patch, Exploit) sharing the static-analysis layer, code reorganization, and engagement memory. ```json { "name": "S11 — Smart Contract Audit Harness", "nodes": [ { "name": "Contract Ingest", "type": "n8n-nodes-base.manualTrigger", "position": [200, 300], "notes": "Load Solidity source + dependencies into the harness" }, { "name": "Code Reorganization", "type": "n8n-nodes-base.set", "position": [420, 300], "notes": "Heimdallr function-level reorganization: split to function units + call graph context" }, { "name": "Static Analysis (Slither/Mythril/Semgrep)", "type": "n8n-nodes-base.executeCommand", "position": [640, 200], "notes": "Taint tracking, pattern detection, symbolic execution → structured candidates" }, { "name": "Engagement Memory", "type": "n8n-nodes-base.set", "position": [640, 400], "notes": "Contracts scanned, candidates found, hypotheses verified, exploits built" }, { "name": "LLM Semantic Reasoning", "type": "n8n-nodes-base.set", "position": [860, 300], "notes": "Intent + exploitability judgment on candidates. Heuristic scaffold for business logic." }, { "name": "Vulnerability Hypothesis", "type": "n8n-nodes-base.set", "position": [1080, 300], "notes": "Candidate finding with confidence + rationale" }, { "name": "Cascaded Verification", "type": "n8n-nodes-base.set", "position": [1300, 300], "notes": "Static re-check → test suite → exploit re-run → formal proof. Eliminates FPs." }, { "name": "DETECT: Finding Output", "type": "n8n-nodes-base.set", "position": [1520, 180], "notes": "Severity, location, rationale, PoC reference, remediation hint" }, { "name": "EXPLOIT: Foundry PoC", "type": "n8n-nodes-base.executeCommand", "position": [1520, 300], "notes": "forked mainnet: setup → attack tx → verify. tx hash, state delta, $ impact" }, { "name": "PATCH: Generate Fix", "type": "n8n-nodes-base.set", "position": [1520, 420], "notes": "LLM generates diff → gates: Slither clean, tests pass, PoC fails, formal holds" }, { "name": "Human Approval Gate", "type": "n8n-nodes-base.set", "position": [1740, 420], "notes": "Auditor reviews verified patch. Harness does NOT deploy." } ], "connections": { "Contract Ingest": { "main": [[{ "node": "Code Reorganization", "type": "main", "index": 0 }]] }, "Code Reorganization": { "main": [[{ "node": "Static Analysis (Slither/Mythril/Semgrep)", "type": "main", "index": 0 }], [{ "node": "Engagement Memory", "type": "main", "index": 0 }]] }, "Static Analysis (Slither/Mythril/Semgrep)": { "main": [[{ "node": "LLM Semantic Reasoning", "type": "main", "index": 0 }]] }, "Engagement Memory": { "main": [[{ "node": "LLM Semantic Reasoning", "type": "main", "index": 0 }]] }, "LLM Semantic Reasoning": { "main": [[{ "node": "Vulnerability Hypothesis", "type": "main", "index": 0 }]] }, "Vulnerability Hypothesis": { "main": [[{ "node": "Cascaded Verification", "type": "main", "index": 0 }]] }, "Cascaded Verification": { "main": [[{ "node": "DETECT: Finding Output", "type": "main", "index": 0 }], [{ "node": "EXPLOIT: Foundry PoC", "type": "main", "index": 0 }], [{ "node": "PATCH: Generate Fix", "type": "main", "index": 0 }]] }, "PATCH: Generate Fix": { "main": [[{ "node": "Human Approval Gate", "type": "main", "index": 0 }]] } } } ``` **Reading the diagram**: Left to right. Source contracts are reorganized into function-level units (Heimdallr's innovation) and fed to the static-analysis layer. Static tools produce structured candidates; the LLM reasons about them with a heuristic scaffold for business logic. Hypotheses pass through cascaded verification, which eliminates false positives. Verified findings branch into three modes: Detect produces the finding report, Exploit builds a Foundry PoC on forked mainnet, Patch generates a fix that must survive the verification gates and a human approval gate. Engagement memory persists across all modes. --- ## Diagram 2 — Why LLMs Alone Fail: The Static-Plus-LLM Pipeline **Type**: Mermaid (flowchart) **Purpose**: Shows the three failure modes of LLM-only auditing and how pairing with static analysis fixes each. ```mermaid flowchart TD SRC["Solidity source (5K–50K LOC, dozens of files)"] subgraph FAIL["LLM-only path — three failure modes"] direction TB HALL["Hallucination on EVM semantics (overflow wraps at 2^256, transfer = 2300 gas)"] CTX["Context overflow on large codebases (compaction drops the storage var 40 files away)"] FP["False positives on benign patterns (flags every external call as reentrancy)"] end subgraph FIX["Harness path — static + LLM"] direction TB SLITHER["Slither: taint tracking, 90+ detectors"] MYTH["Mythril: symbolic execution"] SEMG["Semgrep: custom Solidity rules"] DEDUP["Dedup candidates → structured list"] LLM["LLM: intent + exploitability in context, NOT from raw source"] VERIFIED["Verified hypothesis"] end SRC -->|"naive: feed raw to LLM"| FAIL SRC -->|"harness: static first"| SLITHER SRC --> MYTH SRC --> SEMG SLITHER --> DEDUP MYTH --> DEDUP SEMG --> DEDUP DEDUP --> LLM --> VERIFIED style FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080 style FIX fill:#0d1b2a,stroke:#1b4f72,color:#e4e4e8 style LLM fill:#14141f,stroke:#5eead4,color:#5eead4 style VERIFIED fill:#0d2818,stroke:#1e8449,color:#82e0aa ``` **Reading the diagram**: The left path (LLM-only) hits three structural failures — semantic hallucination, context overflow, false-positive flooding. The right path (harness) runs static analysis first: Slither for taint and patterns, Mythril for symbolic execution, Semgrep for custom rules. Candidates are deduplicated and routed to the LLM, which reasons about intent and exploitability starting from structured candidates (not raw source). The LLM's job changes from "find the bug" (hard, hallucination-prone) to "is this candidate real and exploitable in context" (tractable, verifiable). --- ## Diagram 3 — Invariant Extraction for Business-Logic Bugs **Type**: Mermaid (flowchart) **Purpose**: The business-logic detection strategy — extract intended invariants, check whether code enforces them, identify exploitable gaps. Static analysis alone cannot do this because it checks patterns, not intent. ```mermaid flowchart TD SRC["Protocol source + documentation/comments"] EXTRACT["Invariant extraction (LLM + heuristic scaffold)"] INV["Candidate invariants: 'deposits sum == vault balance' 'governance proposal cannot execute same-tx' 'oracle price is TWAP over N blocks'"] FORMAL["Formalize each invariant → runtime assertion or prover spec"] VERIFY["Verify: runtime fuzzing · symbolic exec · formal proof"] VIOL["Invariant violation found"] CONFIRM["LLM confirmation: is this economically exploitable? (flash-loan reachable = critical)"] FINDING["Confirmed logic finding"] SRC --> EXTRACT --> INV --> FORMAL --> VERIFY VERIFY -->|"violation"| VIOL --> CONFIRM CONFIRM -->|"exploitable"| FINDING CONFIRM -->|"theoretical only"| DEGRADE["Downgrade / log"] STATIC["Static analysis (Slither/Mythril)"] STATIC -.->|"checks patterns, NOT intent"| MISS["Cannot find logic bugs (Beanstalk governance, oracle manipulation)"] style EXTRACT fill:#14141f,stroke:#5eead4,color:#5eead4 style CONFIRM fill:#14141f,stroke:#5eead4,color:#5eead4 style FINDING fill:#0d2818,stroke:#1e8449,color:#82e0aa style MISS fill:#2a0d0d,stroke:#a00000,color:#f08080 style DEGRADE fill:#2a1810,stroke:#a04000,color:#f0a868 ``` **Reading the diagram**: The harness reads the protocol source plus its documentation and comments (which often state intended invariants in plain language). The LLM, scaffolded by domain heuristics, extracts candidate invariants. Each is formalized into a checkable property — a runtime assertion, a fuzz target, or a formal spec. Verification runs fuzzing, symbolic execution, or formal proof. When a violation is found, the LLM confirms whether it is economically exploitable: a violation reachable via flash loan in one transaction is critical; a violation requiring 51% token ownership is theoretical. The lower path shows why static analysis alone misses logic bugs — it checks patterns, not the relationship between code and intent. --- ## Diagram 4 — The Exploit Chain PoC Structure **Type**: Mermaid (flowchart) **Purpose**: The three-phase structure of a proof-of-concept exploit on forked mainnet, and the structured evidence it produces. ```mermaid flowchart LR subgraph SETUP["1. Setup"] FORK["Fork mainnet at block N"] FUND["Fund attacker account"] DEPS["Deploy prerequisites (malicious token, fake oracle)"] end subgraph ATTACK["2. Attack transaction"] CALL["Execute exploit (reentrancy / flash loan / governance)"] end subgraph VERIFY["3. Verification"] ASSERT["Assert: attacker balance up"] ASSERT2["Assert: protocol balance down"] IMPACT["Calculate $ impact at fork-block prices"] end subgraph EVIDENCE["Structured evidence"] TX["tx hash"] STATE["state before/after"] TRACE["call trace"] DOLLARS["economic impact"] POC["PoC file (reproducible)"] end SETUP --> ATTACK --> VERIFY --> EVIDENCE style SETUP fill:#0d1b2a,stroke:#1b4f72,color:#e4e4e8 style ATTACK fill:#2a0d0d,stroke:#a00000,color:#f08080 style VERIFY fill:#0d2818,stroke:#1e8449,color:#82e0aa style EVIDENCE fill:#14141f,stroke:#5eead4,color:#5eead4 ``` **Reading the diagram**: A PoC exploit has three phases. Setup forks mainnet at a specific block (reproducing the on-chain state under which the vulnerability exists), funds the attacker, and deploys any prerequisite contracts. The attack transaction executes the exploit — a reentrancy callback, a flash-loan borrow-manipulate-repay sequence, a governance proposal + vote + execute. Verification asserts the exploit succeeded and calculates the dollar impact. The output is structured evidence: transaction hash, state before and after, the full call trace, the economic impact in token amounts and dollars, and the reproducible PoC file. This evidence is what makes the finding undeniable — a client can run `forge test` and see the vault drain. --- ## Diagram 5 — Cascaded Verification for Patch Quality **Type**: Mermaid (flowchart) **Purpose**: The four-gate cascade that a generated patch must survive. A patch that fails any gate is rejected or regenerated. The cascade is what makes the patch trustworthy. ```mermaid flowchart TD PATCH["Generated patch (LLM-produced diff)"] G1{"Gate 1: Static re-check Slither/Mythril on patched code"} G1PASS["Original finding gone? No new findings?"] G1FAIL["REJECT — patch incomplete or introduces new issue"] G2{"Gate 2: Test suite + property tests"} G2PASS["All tests pass?"] G2FAIL["REJECT — patch breaks intended behavior"] G3{"Gate 3: Exploit re-run PoC against patched code"} G3PASS["Exploit now fails?"] G3FAIL["REJECT — patch does not address actual attack path"] G4{"Gate 4: Formal verification (if feasible)"} G4PASS["Property holds?"] G4FAIL["REJECT — formal property violated"] APPROVED["Verified patch → human approval gate"] HUMAN["Auditor reviews diff, rationale, gate results"] DEPLOY["Approved → deployment (harness does NOT deploy)"] PATCH --> G1 G1 --> G1PASS G1PASS -->|"yes"| G2 G1PASS -->|"no"| G1FAIL G2 --> G2PASS G2PASS -->|"yes"| G3 G2PASS -->|"no"| G2FAIL G3 --> G3PASS G3PASS -->|"yes"| G4 G3PASS -->|"no"| G3FAIL G4 --> G4PASS G4PASS -->|"yes / N/A"| APPROVED G4PASS -->|"no"| G4FAIL APPROVED --> HUMAN --> DEPLOY style PATCH fill:#14141f,stroke:#5eead4,color:#5eead4 style G1FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080 style G2FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080 style G3FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080 style G4FAIL fill:#2a0d0d,stroke:#a00000,color:#f08080 style APPROVED fill:#0d2818,stroke:#1e8449,color:#82e0aa style DEPLOY fill:#0d2818,stroke:#1e8449,color:#82e0aa style HUMAN fill:#2a1810,stroke:#a04000,color:#f0a868 ``` **Reading the diagram**: A generated patch enters at the top and must pass four gates in sequence. Gate 1: static analysis on the patched code confirms the original finding is gone and no new findings appeared. Gate 2: the protocol's test suite (or harness-generated property tests from S11.2 invariants) all pass — the patch did not change behavior. Gate 3: the exploit PoC from S11.3 is re-run against the patched code and must now fail — the specific attack no longer works. Gate 4: where the property is formally expressible, a prover confirms the invariant holds. A patch that survives all four gates is verified but still requires human approval before deployment. The human gate catches what automation cannot — changes to economic behavior that require the team's judgment. --- ## Diagram 6 — EVMbench Taxonomy and the Three Modes **Type**: Mermaid (flowchart) **Purpose**: Maps EVMbench's 117 vulnerabilities across 5 classes to the three evaluation modes, showing how Detect/Patch/Exploit are scored independently. ```mermaid flowchart TD BENCH["EVMbench 117 vulnerabilities · 40 repositories"] subgraph CLASSES["Vulnerability classes"] REENT["Reentrancy"] INT["Integer overflow/underflow"] ACCESS["Access control"] FLASH["Flash loan / oracle"] LOGIC["Business logic"] end subgraph MODES["Three evaluation modes"] DETECT["DETECT mode recall: of 117, how many found?"] PATCH["PATCH mode quality: fix removes bug, preserves behavior?"] EXPLOIT["EXPLOIT mode success: working PoC runs on fork?"] end BENCH --> CLASSES CLASSES --> MODES HEIM["Heimdallr anchor: 92.45% detection · $2.31/10K LOC 17/20 real-world attacks reconstructed"] HEIM -.->|"the bar"| MODES style BENCH fill:#14141f,stroke:#5eead4,color:#5eead4 style DETECT fill:#0d2818,stroke:#1e8449,color:#82e0aa style PATCH fill:#0d2818,stroke:#1e8449,color:#82e0aa style EXPLOIT fill:#0d2818,stroke:#1e8449,color:#82e0aa style HEIM fill:#2a1810,stroke:#a04000,color:#f0a868 ``` **Reading the diagram**: EVMbench's 117 vulnerabilities span five classes — reentrancy, integer overflow, access control, flash loan/oracle, and business logic. Each vulnerability is scored independently across three modes: Detect (did the agent find it?), Patch (did the fix work without breaking behavior?), Exploit (did the agent build a working PoC?). A harness can score well on Detect and poorly on Exploit — finding bugs is easier than exploiting them. Heimdallr's 92.45% detection rate at $2.31 per 10K LOC is the bar the harness is measured against. The next module (S12) covers running against this benchmark in detail.