This is a follow-up to Part 1, where I benchmarked six frontier models on real EigenLayer audit findings. If you haven’t read it, the one-line summary is below.

---

Where Part 1 left off

In Part 1, I built a benchmark out of 14 real audit-fix commits from EigenLayer and ran six frontier models against them as autonomous agents. The headline result surprised a lot of people who expected the story to be about recall:

The false-positive problem, not the recall problem, is the bottleneck for LLM-driven auditing today.

The best model (Claude Opus) rediscovered 53% of the real findings, genuinely impressive with no hints and no file paths. But it did so while emitting ~8.8 unmatched findings per task, for a precision of 16%. Even the most disciplined model, GPT-5.5, sat at 30% precision. In other words: the models can find bugs, but every real finding arrives buried under three to eight plausible-sounding ones that a human has to read, chase down, and dismiss. At audit scale, that triage cost is the whole ballgame.

I ended Part 1 with a sketch of the fix: a verification layer that would make each claimed finding prove itself with executable code, so unverified noise never reaches a human.

I built it. It’s called Forge Proof, it’s open source (github.com/antojoseph/botsec), and this post is about how it works and what it found.

The design shifted along the way. Part 1 imagined spinning up forked-mainnet sandboxes and running generated proof-of-concept exploits. That works, but I found something stronger sitting one level up: formal verification. Instead of running one concrete exploit and hoping it’s representative, symbolic execution searches the entire input space and either hands you a concrete attack or proves no attack exists. Where the math gets too hard for a solver, Forge Proof falls back to fuzzing. The result is a pipeline where a finding is reported only if it comes with a machine-checked exploit, or an explicit, labeled reason it couldn’t be checked.

The core idea: prove-or-discard

Forge Proof is two stages, and each is a precision gate.

Stage 1: Find. Read the code and propose vulnerabilities an unprivileged attacker could exploit. Every proposed threat must carry a TRACE: the exact chain of code locations the attack travels through. No trace, no finding.

Stage 2: Prove. Hand each surviving threat to a symbolic-execution engine that searches for a real exploit. It returns concrete inputs that break the contract, a machine-checked proof, or the finding dies here.

A finding has to clear both gates to reach a human. Gate 1 is cheap and kills vague, unfalsifiable “slop.” Gate 2 is expensive and decisive: it’s the difference between “this looks vulnerable” and “here is the exact input that drains the pool.”

The whole thing is built on the Claude Agent SDK as a set of specialized agents, with deterministic static analysis doing the heavy lifting wherever an LLM isn’t actually needed.

Stage 1a: Pre-computation (hand the model a map, not a pile of files)

Drop an LLM into a raw repository and it reads files more or less blindly. It loses the thread across file boundaries, forgets what it saw twenty files ago, and hallucinates structure that isn’t there. The bigger the codebase, the worse it gets, and DeFi protocols are big.

So before any model runs, Forge Proof does a pass of deterministic static analysis over the Solidity compiler’s AST (forge build --build-info). No model, no token cost, no hallucination, just facts extracted from the code, in about a thousand lines with zero external dependencies. For every contract it builds:

• Call graph: internal and external calls, cross-contract resolution, low-level calls.
• State-variable map: for each variable, who reads it, who writes it, its type and visibility.
• Function summaries: visibility, modifiers, state read/written, calls made.
• Operation ordering: execution order within each function, which is what you need to catch checks-effects-interactions violations (the classic “acts before it verifies”).
• Auth checks: msg.sender conditions from modifiers and inline require/if-revert.
• Data dependency: transitive variable influence with taint tracking, so the agent can see how attacker-controlled input reaches a sensitive sink.

This is the mental model a good human auditor builds in their head before reading a single function closely, made explicit and machine-readable.

The payoff isn’t just quality, it’s context economy. Instead of one giant prompt, each contract gets its own JSON file in a code map, plus four global files (inheritance, call graph, state vars, data dependencies). The threat-modeling agent reads them on demand via file tools. For an 800-contract protocol, that’s ~42 targeted files instead of a single 9 MB blob, and the system prompt stays around 5 KB regardless of codebase size. A small model (Haiku) also classifies each contract’s type (vault, lending pool, DEX, staking) so the agent knows which invariants are even worth checking.

One unglamorous but important detail: the AST pass reads the test/script directory paths out of foundry.toml and excludes them. Before I added that filter, 81% of the agent’s investigation questions were about test-harness setUp() methods. Filtering test contracts out of the analysis was one of the single biggest quality improvements in the project.

Stage 1b: Threat modeling and the TRACE

Now the agentic part. An Opus agent reads the code map and hunts for attack paths, using a set of systematic cross-reference patterns: CEI timelines, reverse cross-referencing, source-to-sink tracing. Two design choices do most of the work:

Untrusted-actor focus. The agent is explicitly told to skip admin/owner misconfiguration scenarios and focus only on what an unprivileged attacker can do. Admin-misconfig “findings” (“if the owner sets a bad value, funds are at risk”) are the single largest source of audit noise, and they’re almost never what a bug bounty pays for. Cutting them at the prompt level removes a huge class of false positives before verification even starts.

The TRACE requirement. Every threat the agent proposes must include a TRACE: the concrete chain of code locations, with file:line references, that an attack would traverse. Here’s a real one, lightly annotated, for an arbitrary-call bug (a classic “confused deputy,” where the contract executes attacker-supplied instructions using its own authority):

[1] flashLoan(target, data)  — lets the caller hand in any call for the pool to run   Pool.sol:45
[2] pool executes target.call(data) — under its OWN identity                          Pool.sol:52
[3] attacker passes approve(attacker, MAX) → pool authorizes the attacker              Token
[4] attacker transfers out everything the pool holds                                   Pool.sol:61

The TRACE is the whole trick for Gate 1. A finding isn’t a sentence of suspicion; it’s a verifiable path. If the model can’t lay out the steps, there’s nothing to check, and the finding is dropped by the anti-slop filter. Two more synthesis filters run alongside it: a self-contradiction filter downgrades threats whose own description is mostly exonerating language (the model talking itself out of its own finding), and deduplication merges findings that overlap by more than 50%. What survives is ranked by severity × confidence.

Stage 2: Formal verification with Halmos

This is where a “finding” becomes a “proof.” Three terms, in case symbolic execution isn’t your daily driver:

• Property: a rule that must always hold. For a lending pool: no sequence of calls lets anyone withdraw more than they deposited.
• Symbolic execution: run the contract with its inputs left as symbols rather than fixed numbers. Each execution path becomes a set of logical constraints over those symbols. The tool here is Halmos, a symbolic execution engine for EVM bytecode.
• SMT solver: the engine underneath (bitwuzla / Z3-class) that searches those constraints for any assignment of inputs that would violate the property.

The verifier agent (Opus, with a Halmos skill preloaded so it knows the solver’s quirks and strategies) discovers any existing tests first, then writes check_-prefixed Halmos test functions, compiles them, runs the solver, and interprets the result:

• VIOLATION → the solver returns concrete inputs that break the property. That output isn’t a hint; it is the exploit. This is why precision jumps: a reported finding comes with a working attack.
• VERIFIED → no violating input exists within the bounds. The property is proven to hold, not merely “untested so far.”

Here’s a real (trimmed) property from the benchmark, for the arbitrary-call bug above:

/// @custom:halmos --solver-timeout-assertion 10000
contract TrusterVerification is SymTest, Test {
    // ...setUp deploys the pool with 1,000,000 tokens...

    function check_pool_cannot_approve_external_addresses() public {
        address attacker = address(0xBAD);
        // Before: pool has approved the attacker nothing
        assertEq(token.allowance(address(pool), attacker), 0);

        // The attack: borrow 0, but make the pool call approve(attacker, max)
        bytes memory data = abi.encodeWithSelector(
            token.approve.selector, attacker, type(uint256).max
        );
        pool.flashLoan(0, attacker, address(token), data);

        // Property: the pool must NOT have approved the attacker
        assertEq(token.allowance(address(pool), attacker), 0,
                 "Pool should not have approved tokens to attacker");
    }
}

Halmos runs this symbolically and reports VIOLATION, because the pool does approve the attacker for type(uint256).max. The counterexample is the calldata that does it. You don’t argue about whether the bug is real; you run it.

The contrast with the Part 1 models is the point. Unit tests check the handful of cases you thought of. The benchmark models pattern-match what they’ve seen. Symbolic execution checks the whole input space within its bounds and hands you the breaking input.

When a proof is impossible: diagnose, then fuzz

Symbolic execution has a hard wall: nonlinear 256-bit arithmetic. Multiplying and dividing large symbolic integers (the math behind AMM pricing, share/asset conversions, virtual prices) blows up the solver. A naive setup just hangs at the timeout and you learn nothing.

Forge Proof treats a timeout as a diagnosable event, not an answer. When Halmos stalls, the verifier inspects why:

• Nonlinear/unsolvable (e.g. mulDivDown on symbolic 256-bit values) → don’t wait out the clock. Fall back immediately.
• Merely a large search space → narrow the symbolic input types and retry.

The fallback is Foundry fuzzing: throw ~1,000,000 randomized inputs at the same property. It’s not a mathematical proof, but it’s strong empirical evidence, and it still surfaces a concrete breaking input when one exists.

The payoff is that there are no silent failures. Every property ends in one of three labeled states (proven, broken with a counterexample, or fuzz-tested), and the report says which. This is the same discipline I leaned on in Part 1: an evaluation you can’t inspect is an evaluation you can’t trust.

Results: Damn Vulnerable DeFi v4

I ran Forge Proof end-to-end against Damn Vulnerable DeFi v4, the standard benchmark of deliberately-broken contracts that the security community uses to evaluate tooling.

Detection:     18/18 challenges — 100% (19 distinct threats; Shards has two)
Halmos proofs: 16 property violations with concrete counterexamples
Verified safe:  8 properties mathematically proven to hold
Timeouts:       0 — all 24 symbolic tests finished within solver bounds
Cost:          $10.81  ($4.18 threat model + $6.63 verification)
Runtime:       ~2 hours
Config:        Halmos 0.3.4, bitwuzla solver, loop bound 3, 10s solver timeout

A few of the machine-proven findings, in plain terms:

• Side Entrance: flash-loan deposit drain. The pool only checks that its ETH balance didn’t decrease, but the repayment path (deposit()) also credits the repayer a withdrawable balance. Borrow, “repay” via deposit, then withdraw. Counterexample: a loan of ~4.6 ETH drains the pool.
• Truster: arbitrary call. The confused-deputy bug above. The pool executes attacker-supplied calldata under its own identity, so the attacker makes it approve(attacker, ∞) and walks the tokens out.
• Token Bridge: inverted authorization. A single comparison operator is backwards: the check that’s supposed to authorize withdrawals does the exact opposite. The legitimate bridge path reverts, and an unauthorized caller succeeds. One flipped ==/!= and the whole authorization is upside down, exactly the kind of one-character logic bug that pattern-matching misses and a solver catches instantly.
• Unstoppable: donation DoS. Send one wei of the token straight to the vault, bypassing deposit(). Now totalAssets() != totalSupply forever, every flash loan reverts, and the vault is permanently bricked. Cost of attack: one wei. Proven with a counterexample.

The honest split

Here’s the part I care most about getting right, because it’s the same intellectual honesty Part 1 tried to model.

Of the 18 challenges, 8 carry a Halmos proof (16 property violations across them) and 10 were confirmed by deep code review rather than a machine proof. Why the split? The code-review cases depend on external systems the solver can’t reproduce on its own within bounds: Uniswap V1/V2/V3 AMM math, Curve virtual-price calculations, Gnosis Safe proxy factories, ERC-4626 share inflation, raw calldata ABI encoding. Halmos verifies properties of individual contracts; multi-contract attack flows that route through third-party protocol math need integration mocks that were out of scope for this run.

So the correct claim is not “100% of DVD proven mathematically.” It’s “100% detected; the exploitable-in-isolation subset proven with counterexamples; the rest confirmed by analysis, and every finding is labeled with how it was established.” A tool that says “I found it but couldn’t machine-prove it” is far more useful than one that blurs the line.

Beyond the benchmark

Forge Proof has also run against real DeFi protocols with active bug-bounty programs (findings responsibly disclosed):

Protocol	Threat model	Verification	Cost
Alpha	8 threats (2 med, 6 low)	8/8 confirmed, 10 fuzz tests	~$22
Gamma	14 threats (3 med, 11 low)	19 Halmos proofs, 3 violations, 15 fuzz tests	~$12
Delta	17 threats (1 high, 3 med, 13 low)	11 Halmos proofs, 1 violation, 6 fuzz tests	~$13

The takeaway isn’t the raw counts. It’s that a full verified pass on a production protocol costs the price of lunch and finishes while you get coffee.

Design decisions worth stealing

A few things generalize beyond smart contracts, to anyone building LLM agents over large codebases:

• Compute structure deterministically; let the LLM reason over it. The expensive, hallucination-prone model should never have to reconstruct a call graph it can get for free from the compiler. Static analysis up front makes the agent both cheaper and more reliable.
• File-based context beats a mega-prompt. Per-contract files read on demand keep the prompt tiny and let the agent load only what’s relevant. Context size stops scaling with repo size.
• Make findings falsifiable by construction. The TRACE requirement is just “show your work, with line numbers.” It’s astonishing how much slop that one rule removes.
• A timeout is not a result. Diagnosing why a verifier stalled, and switching strategies, is the difference between a tool that quietly drops hard cases and one you can trust.
• Label your confidence. Proven vs. fuzz-tested vs. code-review-confirmed. Never let the reader guess how sure the machine is.

Limitations

Stated plainly:

• Bounded proofs. Loop bound 3, 10-second solver timeout. Proofs hold within those bounds. That’s standard for symbolic execution and still far stronger than an unverified claim, but it isn’t unbounded.
• No cross-contract symbolic execution. Halmos proves properties of individual contracts. Governance takeovers, oracle-manipulation chains, and other multi-contract flows fall to the code-review path.
• Mocks vs. full contract trees. Some tests use mock contracts that replicate the vulnerable pattern rather than the full integration. Core logic is identical; integration-level issues could differ.
• One benchmark, plus a few private protocols. DVD is curated and known-exploitable. Whether the same numbers hold on messier, uncurated production code is exactly the open question (see below).

What’s next

The obvious next experiment writes itself: re-run Forge Proof’s verification layer over the Part 1 EigenLayer benchmark and measure the precision lift directly. Part 1 established the recall/precision numbers for raw models; the clean comparison is what those precision numbers become once every finding has to pass Gate 1 and Gate 2. That’s an apples-to-apples measurement I haven’t run yet, and it’s the number I most want to know.

Two other directions I’m excited about:

• A verifier is a reward signal. A sandbox that mechanically decides whether an exploit is real is exactly the clean, hard-to-game signal you’d want to train a security model with, not just evaluate one.
• Verification is generation-heavy. Write a property, compile, solve, interpret, revise: many candidate proofs per finding. This is precisely the regime where cheap, fast inference changes what’s affordable: more candidate properties per bug, more bugs verified per dollar.

Part 1 measured the problem. Forge Proof is my attempt to build the fix. If you want to poke at it, or tell me where the honest-split line should actually be drawn, the code is at github.com/antojoseph/botsec.

— Anto