Module: S11 — Smart Contract Audit Harnesses · Duration: ~90 minutes
Format: Verbatim transcript. Cues [SLIDE N] map to 03-slide-deck.html.
[SLIDE 1 — Title]
This is Module S Eleven: Smart Contract Audit Harnesses. Ninety minutes. The first module of Pillar Four, and where the harness architecture from Pillars One through Three becomes a smart-contract-specific system. Four sub-sections: the EVM audit architecture, business-logic vulnerability detection, exploit chain construction, and patch generation with cascaded verification. By the end you can build a harness that detects, exploits, and patches vulnerabilities in Solidity code, benchmarked against EVMbench's one hundred seventeen curated vulnerabilities.
The core idea: a smart contract security harness operates in three modes — Detect, Patch, Exploit. Detect finds vulnerabilities. Patch generates fixes. Exploit builds and runs proof-of-concept attacks. EVMbench — the benchmark from OpenAI and Paradigm — evaluates agents across exactly these three modes. A harness that only detects is half a harness.
[SLIDE 2 — S11.1: The EVM Audit Architecture]
Sub-section one. The EVM audit architecture. The three modes are the frame: Detect, Patch, Exploit. EVMbench scores all three independently across one hundred seventeen curated vulnerabilities drawn from forty real EVM repositories — reentrancy, integer overflow, access control, flash loan, and business logic classes. You can score well on Detect and poorly on Exploit. Finding bugs is easier than exploiting them, which is easier than fixing them without breaking anything.
[SLIDE 3 — Why LLMs alone fail]
Here is the tempting shortcut that fails. Point a frontier LLM at a Solidity file and ask it to find the bugs. Three structural failures.
First, hallucination on EVM semantics. The EVM has precise, counter-intuitive semantics. Integer overflow wraps at two to the two hundred fifty-sixth power — it does not throw. The transfer function forwards exactly twenty-three hundred gas — not the full gas stipend. Address-this-balance reads the contract's actual 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 systematic, not random, because the model applies general-language intuitions to a domain where those intuitions mislead.
Second, context overflow. 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 five thousand to fifty thousand lines of Solidity across dozens of files. No context window holds that with the precision a security audit demands. Compaction silently drops the storage variable declared forty files away that makes the flash loan path exploitable.
Third, false positives. 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.
[SLIDE 4 — The harness pipeline]
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.
Slither — from Trail of Bits — does taint analysis and detects over ninety vulnerability patterns. Mythril performs symbolic execution to find execution paths that violate safety properties. Semgrep Solidity adds custom rule-based pattern matching. None 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.
The LLM's job changes. It is no longer "find the bug from raw source" — which is hard and hallucination-prone. It is "is this candidate real and exploitable in context" — which is tractable and verifiable. That shift is the entire architecture.
[SLIDE 5 — Heimdallr, the anchor design]
Heimdallr is the anchor system for this module. It achieved a ninety-two point four five percent detection rate at a cost of two dollars and thirty-one cents per ten thousand lines of code in contest-style auditing, and reconstructed seventeen of twenty real-world attacks that occurred after June twenty twenty-five. Three innovations matter for harness design.
First, 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. Nothing else. This minimizes context overhead while preserving the information needed for semantic reasoning.
Second, heuristic reasoning for business logic. For logic vulnerabilities, 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.
Third, cascaded verification to eliminate false positives. Every LLM-produced hypothesis passes through a verification cascade: static analysis re-checks the claim, the test suite runs against the hypothesized vulnerability, 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.
[SLIDE 6 — S11.2: Business Logic Vulnerability Detection]
Sub-section two. Business-logic vulnerability detection. 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.
Consider the twenty twenty-two Beanstalk governance attack — one hundred eighty-two million dollars. 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. The bug is not in any single line. It is in the relationship between the code and the protocol's intended invariants.
Static analysis checks patterns against a catalog of known-bad patterns. It cannot check intent. The harness strategy is invariant extraction: identify what the protocol intends to be always-true, then check whether the code enforces it.
[SLIDE 7 — Invariant extraction]
The invariant extraction pipeline. The harness reads the protocol source plus its documentation and comments — which often state intended invariants in plain language, and the code's comments frequently assert them. The LLM, scaffolded by domain heuristics, extracts candidate invariants. "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."
Each invariant is formalized into a checkable property — a runtime assertion, a fuzz target, or a formal spec. Verification runs: runtime fuzzing, symbolic execution, formal proof. When a violation is found, the LLM confirms whether it is economically exploitable. A violation reachable via flash loan in a single transaction is critical. A violation that requires an attacker to already own fifty-one percent of the token supply is theoretical. That distinction — economically exploitable versus theoretically possible — is what separates a critical finding from a noise entry.
[SLIDE 8 — Flash loan attack paths]
Flash loans. 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. 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 attacker acts as a whale for the duration of one transaction.
The harness detects flash loan paths by tracing data flow from external price or oracle sources through to state-changing operations, and checking whether the price source is manipulable in a single transaction. Spot DEX prices are manipulable — a flash loan can swap into the pool, move the price, exploit the protocol, and swap back. Time-weighted average prices over multiple blocks are resistant — the manipulation cannot persist across blocks within one transaction.
For context budget on large contracts, Heimdallr's function-level reorganization extends along the call graph. If Vault-dot-withdraw calls Oracle-dot-getPrice, and Oracle-dot-getPrice reads from a spot DEX pool, the harness includes all three in the LLM's context with the data-flow edges between them. The model can then reason: the withdrawal amount is computed from a spot price, which is flash-loan manipulable, therefore the withdrawal can be inflated. That is a flash loan attack path, identified by reasoning over the call graph, not by pattern matching.
[SLIDE 9 — S11.3: Exploit Chain Construction]
Sub-section three. 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.
A proof-of-concept exploit has three phases. Setup: fork mainnet at a specific block, fund the attacker account, deploy any prerequisites — a malicious token contract, a flash loan provider, a fake oracle. 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 one transaction. Verification: assert 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.
[SLIDE 10 — Structured exploit evidence]
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 precise on-chain state — the liquidity in a DEX pool, the governance proposal queue, the oracle's last reported price.
Foundry — with forge test dash dash fork-url — is the primary tool. It is fast, supports Solidity-native test writing, and integrates with CI. Hardhat is the alternative for JavaScript or TypeScript toolchains. The harness wraps either as a tool: input is the PoC Solidity file and fork configuration; output is the test result, the transaction trace, the state delta, and the gas used.
The evidence is structured, not narrative. Transaction hash. Block number — the forked block at which the exploit is valid. State before and after. The call trace — the sequence of internal and external calls. Economic impact — token amounts and dollar value at the fork block's prices. The PoC file, reproducible with forge test. This structured evidence is what makes the finding actionable. A client who receives "reentrancy in Vault-dot-withdraw" can argue it is theoretical. A client who receives a transaction trace showing ten thousand ether moved from the vault to the attacker account in a forked-mainnet PoC cannot.
[SLIDE 11 — S11.4: Patch Generation and Cascaded Verification]
Sub-section four. 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.
[SLIDE 12 — The four verification gates]
Every generated patch passes through a cascade of four gates.
Gate one: static analysis re-check. Run Slither and Mythril 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.
Gate two: 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 sub-section two and runs those. A patch that breaks a passing test has failed. It changed behavior, not just security.
Gate three: exploit re-run. The PoC from sub-section three 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.
Gate four: formal verification, where feasible. For properties expressible as formal specs — the sum of deposits is always greater than or equal to the contract balance, only the owner can call setAdmin — run a prover on the patched code. Formal verification is not always feasible; complex economic properties resist formalization. But when it is feasible, it provides the strongest guarantee.
A patch that survives all four gates is verified. But it still requires human approval before deployment. 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.
[SLIDE 13 — The patch-that-fixes-the-PoC trap]
Here is a trap that is easy to miss. The patch that fixes the PoC but not the underlying vulnerability. If the harness's PoC used a ten ether deposit, and the patch adds a check that deposits must be exactly ten ether, the PoC fails but the vulnerability remains. A fifty-ether deposit still exploits it. The exploit re-run gate alone would not catch this — the PoC failed, so the gate passed. But the static-analysis re-check and the formal-verification gate catch it. The static analyzer still flags the reentrancy pattern, and the formal prover still shows the invariant can be violated. This is why the cascade has four gates, not one. The exploit re-run is necessary but insufficient.
[SLIDE 14 — What you take into S12]
The audit harness is operational. You have the three-mode architecture, invariant extraction for business logic, exploit PoCs on forked mainnet with structured evidence, and cascaded patch verification. S Twelve takes this further in three directions. First, benchmarking against EVMbench in detail — the three scores that matter, and the ninety-two percent versus thirty-four percent gap between purpose-built agents and general LLMs on DeFi. Second, Solana and cross-chain security — the account model, the Anchor framework, bridge security. Third, the audit as a deliverable — report structure, severity classification, and the format top firms like Trail of Bits, Consensys Diligence, and OpenZeppelin publish.
[End of script]
# Teaching Script — Module S11: Smart Contract Audit Harnesses **Module**: S11 — Smart Contract Audit Harnesses · **Duration**: ~90 minutes **Format**: Verbatim transcript. Cues `[SLIDE N]` map to `03-slide-deck.html`. --- [SLIDE 1 — Title] This is Module S Eleven: Smart Contract Audit Harnesses. Ninety minutes. The first module of Pillar Four, and where the harness architecture from Pillars One through Three becomes a smart-contract-specific system. Four sub-sections: the EVM audit architecture, business-logic vulnerability detection, exploit chain construction, and patch generation with cascaded verification. By the end you can build a harness that detects, exploits, and patches vulnerabilities in Solidity code, benchmarked against EVMbench's one hundred seventeen curated vulnerabilities. The core idea: a smart contract security harness operates in three modes — Detect, Patch, Exploit. Detect finds vulnerabilities. Patch generates fixes. Exploit builds and runs proof-of-concept attacks. EVMbench — the benchmark from OpenAI and Paradigm — evaluates agents across exactly these three modes. A harness that only detects is half a harness. [SLIDE 2 — S11.1: The EVM Audit Architecture] Sub-section one. The EVM audit architecture. The three modes are the frame: Detect, Patch, Exploit. EVMbench scores all three independently across one hundred seventeen curated vulnerabilities drawn from forty real EVM repositories — reentrancy, integer overflow, access control, flash loan, and business logic classes. You can score well on Detect and poorly on Exploit. Finding bugs is easier than exploiting them, which is easier than fixing them without breaking anything. [SLIDE 3 — Why LLMs alone fail] Here is the tempting shortcut that fails. Point a frontier LLM at a Solidity file and ask it to find the bugs. Three structural failures. First, hallucination on EVM semantics. The EVM has precise, counter-intuitive semantics. Integer overflow wraps at two to the two hundred fifty-sixth power — it does not throw. The transfer function forwards exactly twenty-three hundred gas — not the full gas stipend. Address-this-balance reads the contract's actual 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 systematic, not random, because the model applies general-language intuitions to a domain where those intuitions mislead. Second, context overflow. 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 five thousand to fifty thousand lines of Solidity across dozens of files. No context window holds that with the precision a security audit demands. Compaction silently drops the storage variable declared forty files away that makes the flash loan path exploitable. Third, false positives. 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. [SLIDE 4 — The harness pipeline] 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. Slither — from Trail of Bits — does taint analysis and detects over ninety vulnerability patterns. Mythril performs symbolic execution to find execution paths that violate safety properties. Semgrep Solidity adds custom rule-based pattern matching. None 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. The LLM's job changes. It is no longer "find the bug from raw source" — which is hard and hallucination-prone. It is "is this candidate real and exploitable in context" — which is tractable and verifiable. That shift is the entire architecture. [SLIDE 5 — Heimdallr, the anchor design] Heimdallr is the anchor system for this module. It achieved a ninety-two point four five percent detection rate at a cost of two dollars and thirty-one cents per ten thousand lines of code in contest-style auditing, and reconstructed seventeen of twenty real-world attacks that occurred after June twenty twenty-five. Three innovations matter for harness design. First, 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. Nothing else. This minimizes context overhead while preserving the information needed for semantic reasoning. Second, heuristic reasoning for business logic. For logic vulnerabilities, 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. Third, cascaded verification to eliminate false positives. Every LLM-produced hypothesis passes through a verification cascade: static analysis re-checks the claim, the test suite runs against the hypothesized vulnerability, 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. [SLIDE 6 — S11.2: Business Logic Vulnerability Detection] Sub-section two. Business-logic vulnerability detection. 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. Consider the twenty twenty-two Beanstalk governance attack — one hundred eighty-two million dollars. 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. The bug is not in any single line. It is in the relationship between the code and the protocol's intended invariants. Static analysis checks patterns against a catalog of known-bad patterns. It cannot check intent. The harness strategy is invariant extraction: identify what the protocol intends to be always-true, then check whether the code enforces it. [SLIDE 7 — Invariant extraction] The invariant extraction pipeline. The harness reads the protocol source plus its documentation and comments — which often state intended invariants in plain language, and the code's comments frequently assert them. The LLM, scaffolded by domain heuristics, extracts candidate invariants. "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." Each invariant is formalized into a checkable property — a runtime assertion, a fuzz target, or a formal spec. Verification runs: runtime fuzzing, symbolic execution, formal proof. When a violation is found, the LLM confirms whether it is economically exploitable. A violation reachable via flash loan in a single transaction is critical. A violation that requires an attacker to already own fifty-one percent of the token supply is theoretical. That distinction — economically exploitable versus theoretically possible — is what separates a critical finding from a noise entry. [SLIDE 8 — Flash loan attack paths] Flash loans. 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. 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 attacker acts as a whale for the duration of one transaction. The harness detects flash loan paths by tracing data flow from external price or oracle sources through to state-changing operations, and checking whether the price source is manipulable in a single transaction. Spot DEX prices are manipulable — a flash loan can swap into the pool, move the price, exploit the protocol, and swap back. Time-weighted average prices over multiple blocks are resistant — the manipulation cannot persist across blocks within one transaction. For context budget on large contracts, Heimdallr's function-level reorganization extends along the call graph. If Vault-dot-withdraw calls Oracle-dot-getPrice, and Oracle-dot-getPrice reads from a spot DEX pool, the harness includes all three in the LLM's context with the data-flow edges between them. The model can then reason: the withdrawal amount is computed from a spot price, which is flash-loan manipulable, therefore the withdrawal can be inflated. That is a flash loan attack path, identified by reasoning over the call graph, not by pattern matching. [SLIDE 9 — S11.3: Exploit Chain Construction] Sub-section three. 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. A proof-of-concept exploit has three phases. Setup: fork mainnet at a specific block, fund the attacker account, deploy any prerequisites — a malicious token contract, a flash loan provider, a fake oracle. 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 one transaction. Verification: assert 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. [SLIDE 10 — Structured exploit evidence] 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 precise on-chain state — the liquidity in a DEX pool, the governance proposal queue, the oracle's last reported price. Foundry — with forge test dash dash fork-url — is the primary tool. It is fast, supports Solidity-native test writing, and integrates with CI. Hardhat is the alternative for JavaScript or TypeScript toolchains. The harness wraps either as a tool: input is the PoC Solidity file and fork configuration; output is the test result, the transaction trace, the state delta, and the gas used. The evidence is structured, not narrative. Transaction hash. Block number — the forked block at which the exploit is valid. State before and after. The call trace — the sequence of internal and external calls. Economic impact — token amounts and dollar value at the fork block's prices. The PoC file, reproducible with forge test. This structured evidence is what makes the finding actionable. A client who receives "reentrancy in Vault-dot-withdraw" can argue it is theoretical. A client who receives a transaction trace showing ten thousand ether moved from the vault to the attacker account in a forked-mainnet PoC cannot. [SLIDE 11 — S11.4: Patch Generation and Cascaded Verification] Sub-section four. 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. [SLIDE 12 — The four verification gates] Every generated patch passes through a cascade of four gates. Gate one: static analysis re-check. Run Slither and Mythril 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. Gate two: 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 sub-section two and runs those. A patch that breaks a passing test has failed. It changed behavior, not just security. Gate three: exploit re-run. The PoC from sub-section three 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. Gate four: formal verification, where feasible. For properties expressible as formal specs — the sum of deposits is always greater than or equal to the contract balance, only the owner can call setAdmin — run a prover on the patched code. Formal verification is not always feasible; complex economic properties resist formalization. But when it is feasible, it provides the strongest guarantee. A patch that survives all four gates is verified. But it still requires human approval before deployment. 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. [SLIDE 13 — The patch-that-fixes-the-PoC trap] Here is a trap that is easy to miss. The patch that fixes the PoC but not the underlying vulnerability. If the harness's PoC used a ten ether deposit, and the patch adds a check that deposits must be exactly ten ether, the PoC fails but the vulnerability remains. A fifty-ether deposit still exploits it. The exploit re-run gate alone would not catch this — the PoC failed, so the gate passed. But the static-analysis re-check and the formal-verification gate catch it. The static analyzer still flags the reentrancy pattern, and the formal prover still shows the invariant can be violated. This is why the cascade has four gates, not one. The exploit re-run is necessary but insufficient. [SLIDE 14 — What you take into S12] The audit harness is operational. You have the three-mode architecture, invariant extraction for business logic, exploit PoCs on forked mainnet with structured evidence, and cascaded patch verification. S Twelve takes this further in three directions. First, benchmarking against EVMbench in detail — the three scores that matter, and the ninety-two percent versus thirty-four percent gap between purpose-built agents and general LLMs on DeFi. Second, Solana and cross-chain security — the account model, the Anchor framework, bridge security. Third, the audit as a deliverable — report structure, severity classification, and the format top firms like Trail of Bits, Consensys Diligence, and OpenZeppelin publish. --- [End of script]