sc-verify — Adversarial Verification & PoC Gate (Pipeline Stage 5)

This is the stage that makes the tool worth more than a naked LLM. Anyone can list 50 suspicions; this stage proves or kills each one. A hypothesis becomes a finding only when a concrete proof demonstrates it — an exploit PoC that runs, or a differential test that shows the implementation diverging from spec. Everything else stays a candidate. That discipline is the entire low-false-positive promise.

The crux: a textbook "CRITICAL reentrancy" smell can be non-exploitable (e.g. Solidity 0.8 underflow checks revert the reentrant double-spend). Only building the PoC reveals that. A checklist or one-shot LLM mis-rates it; the gate catches it.

When to Use

• After sc-hypothesize; orchestrator calls this fifth.
• User says: "verify these", "prove it", "write the PoC", "is this real".

Announce

Begin with: "I'm using the sc-verify skill to adversarially verify the hypotheses and build PoCs..."

The prosecutor / defender protocol (per hypothesis)

Run BOTH roles for each kept hypothesis; the burden of proof is on the prosecutor.

Prosecutor — build the proof

• Exploit hypotheses (reentrancy, oracle, slippage, access, …): scaffold and fill a Foundry PoC.

  python skills/sc-verify/scripts/scaffold_poc.py <audit_dir> <H-id>

  Fill the TODOs: deploy the target with real constructor args + minimal mocks, implement the exploit steps from exploit_sketch, and assert the broken invariant (fund loss / insolvency / unauthorized state change). Convention: the test PASSES when the exploit SUCCEEDS — run_verify reads pass==confirmed.
• Math-divergence hypotheses: write a VERBATIM candidate transcription of the contract's arithmetic at verify/diff/<H-id>_candidate.py (copy the Solidity operators 1:1; /→//). The diff_runner compares it to the sc-spec reference over fuzzed + boundary inputs. Also emit the Foundry FFI differential test ( templates/differential.t.sol.template) for the on-chain-bytecode proof where forge exists.

Defender — try to refute

Before accepting any confirmation, rule out every item in the hypothesis's existing_mitigations_to_check, plus:

• Is there a guard the prosecutor ignored (nonReentrant, access control, a require earlier in the flow)? Re-read the chunk and its modifiers.
• Does checked arithmetic / a later check make the exploit revert? (the 0.8 underflow case — verify the PoC actually profits, not just runs).
• Is the behavior a by_design power from the project map? Then it is not a finding (or only the unbounded aspect is).
• Is the location actually reachable by the claimed attacker (call-graph reachability)? If the defender wins, the verdict is rejected (or needs-info) with the reason.

Foundry workspace (one-time, for exploit PoCs)

python skills/sc-verify/scripts/setup_foundry.py <audit_dir>

This auto-selects a mode (recorded in verify/mode.json, honored by run_verify):

• native — the target IS a Foundry project (foundry.toml at its root). PoCs go in <target>/test/_proofhound/ and forge runs in the target root, so its own remappings / lib / fixtures / fork config resolve. Required for integration protocols (GMX, Uniswap, etc.) whose contracts only compile with their deps — this is the P0 fix from the Gamma post-mortem. Mirror an existing target test's imports + fixtures when writing PoCs. (If the downloaded repo lacks its deps, setup tries git submodule update --init; otherwise run the target's own forge install / yarn first.)
• isolated — dependency-free target: a self-contained workspace at .audit/verify/ with copied sources + forge-std. This copies the target sources into verify/src/, installs forge-std, writes foundry.toml (with ffi = true for differential FFI), and smoke-builds. Requires forge (and git). If forge is missing, install Foundry first:
• Windows: download foundry_stable_win32_amd64.zip from the foundry-rs/foundry releases and extract to ~/.foundry/bin (the harness auto-detects that path).
• macOS/Linux/WSL: curl -L https://foundry.paradigm.xyz | bash && foundryup.

PoC convention: write the test to PASS when the finding is demonstrated — the exploit succeeds, or the property violation is shown. run_verify reads pass==confirmed for forge-run PoCs.

Scaling: inline vs fan-out (choose by number of kept hypotheses)

• Few kept hypotheses: inline. Author each PoC yourself as described above.
• Many kept hypotheses: fan-out the PoC AUTHORING (execution stays central):

  python skills/sc-verify/scripts/batch_verify.py <audit_dir> --size 4

  For each verify/batches/batch-NNN.json, spawn an sc-verify-worker subagent in parallel; each authors the PoC artifacts (verify/poc/<id>.t.sol / verify/diff/<id>_candidate.py) and the defender analysis for its few hypotheses — but does NOT execute them. Report progress per batch (Writing PoCs, batch X/N). When all workers finish, run the harness ONCE (below) to execute everything. Centralized execution avoids forge build contention and keeps a single deterministic verdict authority.

Execute & record (harness)

python skills/sc-verify/scripts/run_verify.py <audit_dir>   # default .audit

The harness auto-detects forge (PATH or ~/.foundry/bin). With a workspace present it runs each exploit PoC via forge test; differential proofs always run in Python. This is the single authority that turns authored PoCs into verdicts — run it once, after inline authoring OR after all fan-out workers finish. For each hypothesis the harness locates the proof artifact, runs it (differential in Python; exploit under forge test if installed), writes .audit/verify/<H-id>.json, updates the hypothesis status, and rolls up .audit/verify/summary.json. Verdicts:

• confirmed — green proof. confirmation_strength: onchain-poc (forge green) > python-differential (transcription divergence) > reasoned.
• rejected — parity (math) or the PoC did not demonstrate the exploit (defender wins).
• needs-poc / needs-candidate — prosecutor artifact not written yet.
• needs-execution — PoC written but forge not installed here (run elsewhere).
• needs-info — manual; impact depends on context outside the repo.

Severity (set only on confirmed)

severity = f(impact, likelihood) (matrix in reference.md):

• impact from the targeted invariant's criticality, then adjusted by the proof: a divergence that favors the user is a value leak (keep impact); one that only short-changes users is precision/fairness (cap impact). A reentrancy that reverts (no profit) → rejected, not low.
• likelihood from reachability + attacker prerequisites + capital (flash-loan reachable & unprivileged = high).

Anti-False-Positive Principles (the whole point of this stage)

1. No proof, no finding. confirmed requires a green PoC or a demonstrated divergence — never just a convincing argument.
2. Make the defender work. Every confirmation must survive an explicit attempt to refute it (mitigations, checked-arith reverts, by-design, reachability).
3. Strength is labeled. onchain-poc > python-differential > reasoned; stage 6 can require a minimum strength for the top severities.
4. Rejections are kept with reasons — the audit trail shows what was considered and why it was dropped (this is what auditors trust).

Honesty about environment

With Foundry installed, exploit PoCs execute on real bytecode (onchain-poc strength) — this is the default. Without it, they are written and marked needs-execution (run where forge exists). Differential math proofs always run in Python (python-differential); the Foundry FFI differential test upgrades them to onchain-poc where forge is present. Be explicit in the handoff about each finding's confirmation strength.

Handoff

Tell the orchestrator: confirmed findings with severity and strength, rejected (with reasons), and what still needs execution/PoC/info. Hand the confirmed set to sc-report.