What "verified" means
The agent receives only a vulnerable Solidity/Foundry workspace and must submit one self-contained regression test under test/submission/. A submission earns verified-proof credit only when a deterministic evaluator, running in disposable network-isolated Docker containers, confirms the test compiles on both revisions, fails on the vulnerable revision, and passes on the curator-held fixed revision. This measures executable discrimination, not prose plausibility.
Table 09 · Verified-proof outcomes
Verified proofs per task and condition
| Task (family) | Tool-assisted | Static (no tools) | Budgeted triage |
|---|---|---|---|
| share-inflation (asset/share rounding) | pending | pending | pending |
| reentrancy-withdraw (external-call ordering) | pending | pending | pending |
| uninitialized-treasury (initialization authorization) | pending | pending | pending |
Local feasibility study, 6 replicates per cell; not an official EVMbench score. Cells with no terminal run read "pending", never zero.
Table 10 · Verified-proof rate
Verified-proof rate by condition
| Condition | Agent access | Terminal | Verified | Rate | 95% CI |
|---|---|---|---|---|---|
| Tool-assisted | Bounded search/read + forge build/test feedback, then one submitted proof | 0 | pending | pending | pending |
| Static (no tools) | Full source context (target + provided test harness); no tool feedback | 0 | pending | pending | pending |
| Budgeted triage | A strict budget of four inspect operations, then one submission | 0 | pending | pending | pending |
The CI clusters on three tasks, so intervals are wide by construction. Quality is pending until a condition is fully terminal; pending is never shown as zero. This is an agent-system study, not a model leaderboard.
The local model and runtime, frozen before any run
The requested Qwen/Qwen3.8-27B-FP8 cannot run at FP8 or at its native 262,144-token context in 24 GB of unified memory. The same Qwen3.8-27B model is therefore served at its official Ollama Q4_K_M quantization with a conservative 8,192-token single-request context on an Apple M4 Pro. This is a documented quantization and context adaptation of the requested model, not a different model and not a cloud fallback, and no native long-context performance is claimed.
Table 12 · Model & runtime lock
Frozen local model and runtime
| Field | Value |
|---|---|
| Requested spec | Qwen/Qwen3.8-27B-FP8 |
| Served locally | qwen3.8:27b → alias qwen3.8-27b-local |
| Quantization | Q4_K_M (requested FP8) |
| Architecture | qwen35 · 27.32B params |
| Context length | 262144 native · served at 8192 |
| Runtime engine | Ollama 0.32.14, loopback 127.0.0.1:11435, cloud disabled |
| Host | Apple M4 Pro · 24 GB unified memory · arm64 |
| Sampling | think=false, temperature=1, top_p=0.95, num_predict=4096 |
| Replicates | 6 per cell · seed = 1000 + replicate |
| Harness version | v2 (forge-std-subset test base) |
| Manifest SHA-256 | ec9bb426e93b2300 |
The requested FP8 spec and native 262144-token context do not fit 24 GB; the same model is served at Q4_K_M with an 8192-token context. This is a documented adaptation, not a different model and not a cloud fallback. No native long-context performance is claimed.
Three curated task families
Each task is a small, purpose-built offline fixture of a canonical vulnerability class: an ERC-4626-style first-depositor share inflation, a classic reentrant withdrawal, and an unprotected initializer. The vulnerable workspace is public to the agent; the fixed revision is curator-held and never mounted. Because these are curated fixtures of familiar patterns, they do not establish performance on real audit repositories.
Three conditions over the same tasks
Table 11 · Frozen protocol
Conditions and budgets
| Condition | Agent access | Turn / tool budget | Wall cap |
|---|---|---|---|
| Tool-assisted | Bounded search/read + forge build/test feedback, then one submitted proof | 12 turns / 10 tools | 1200 s |
| Static (no tools) | Full source context (target + provided test harness); no tool feedback | 3 turns / 0 tools | 900 s |
| Budgeted triage | A strict budget of four inspect operations, then one submission | 6 turns / 4 tools | 900 s |
The agent receives only the vulnerable workspace; the fixed revision is never mounted. Foundry ffi and filesystem permissions are disabled in every task.
The agent interacts through a tiny JSON action protocol — read, search, run (forge build/forge test only), write (to test/submission/ only), and final. It is never given a shell, and it is told the exact test-harness contract it must satisfy.
Operational telemetry, kept separate from quality
Table 13 · Operational telemetry
Wall time, generated tokens, and localisation
| Metric | Value |
|---|---|
| Median wall time / run | pending |
| Total collection wall time | pending |
| Generated tokens (total) | pending |
| Generated tokens (median / run) | pending |
| Tool calls (total) | pending |
| Source localised (tool-enabled runs) | pending |
Operational telemetry is kept separate from the verified-proof endpoint. Wall time and generated tokens do not prove correctness. Pending cells are never shown as zero.
Fully local and sandboxed
During every run the model endpoint is a loopback-only Ollama server with cloud disabled; the agent has no browser, web, provider API, RPC, wallet, or live chain. Untrusted build and test execution runs in a disposable Docker container with --network none, a read-only root filesystem, all Linux capabilities dropped, no-new-privileges, bounded CPU/memory/PIDs, a single workspace bind mount, a non-root user, and no mounted credentials. Foundry FFI and filesystem permissions are disabled in every task.
What this pilot does not claim
Six runs per cell over three task clusters give a distribution and a bootstrap interval, but three clusters make those intervals wide; this study does not license a decisive between-condition or between-system claim. The tasks are curated fixtures of familiar patterns that may be represented in training data; the 8,192-token context is a hardware constraint, so long-context behaviour is untested; and Q4_K_M quantization, the Ollama runtime, thinking-disabled decoding, and the tool prompting are material confounds recorded in every run ledger. A patch-differentiating test shows an executable regression check exists, not that a full audit was performed.