merge(search-with-proof): verification-architecture doc + proof-arm-opencode brief [skip ci]

Co-Authored-By: Claude Opus 4.8 <[email protected]>

.kiro/specs/proof-arm-opencode/brief.md

@@ -0,0 +1,87 @@
+# Brief: OpenCode-MCP proof arm (follow-up to search-with-proof)
+
+Status: brief / not yet specced. Proposed 2026-10-07 by the maintainer. Builds on
+`search-with-proof` (see `../search-with-proof/verification-architecture.md`).
+
+## Motivation
+
+The search arm (directed, Cairn-inspired) works. The **proof-authoring** last mile is the drag:
+
+1. **Safety-classifier refusals.** Authoring exploit demos repeatedly tripped a safety classifier
+   this session when exploit payloads or step-by-step attack prose passed through the model or a
+   tool prompt. The mitigation so far (keep payloads on disk, treat demos as opaque) is a workaround,
+   not a fix, and it limits how directly the proof model can reason about the exploit.
+2. **Nondeterministic wiring.** The agent authors a demo but intermittently mis-wires the app to
+   the oracle fixture (served directory for path, database URL for SQL), so a demonstrable pair
+   comes back inconclusive until a retry. Each miss has cost a paid run.
+
+Proposal: drive the proof with an **agentic coding tool (OpenCode MCP)** running **inside gVisor**,
+using a model chosen for exploit authoring rather than one that refuses it, and **learn** the
+proof-authoring policy with DSPy from **traces logged in OpenObserve**.
+
+## Shape
+
+- **Search model:** DeepSeek (current). Good at the directed fact/intent search.
+- **Proof model:** GLM 5.3 (Anthropic-recommended) and/or an abliterated model via
+  `ABLITERATION_BASE_URL` (`abliterated large v2`). The abliterated model authors exploit **demos**
+  without the refusals that block a safety-trained model on this defensive task.
+- **Proof driver:** OpenCode MCP (github.com/AlaeddineMessadi/opencode-mcp) as the agentic
+  demo-author, running inside the gVisor verification task so the exploit-authoring is sandboxed.
+- **Learning:** DSPy compiles/optimizes the proof-authoring program (demo schema, wiring, steps)
+  from past traces, instead of the per-family hand-guidance we keep adding (which is now hitting
+  the prompt character budget — a signal the hand-rule approach is near its limit). Matches the
+  maintainer's "learned decisions, not hand-tuning" direction.
+- **Tracing:** proof runs (reason/explore/author/verify, timings, outcomes, error classes) log to
+  **OpenObserve AI** at `OPENOBSERVE_URL` (org `OPENOBSERVE_ORG`, stream `OPENOBSERVE_TRACES_STREAM`).
+  DSPy consumes these traces as its training signal.
+- **Credentials:** stored in `.env` like the existing keys, referenced by name only:
+  `ABLITERATION_API_KEY`, `ABLITERATION_BASE_URL`, `ABLITERATION_MODEL`, `OPENOBSERVE_URL`,
+  `OPENOBSERVE_ORG`, `OPENOBSERVE_TRACES_STREAM`, `OPENOBSERVE_TOKEN`. No secret value ever enters a
+  tracked file, a prompt, a log stream, or a commit.
+
+## The trust-domain decision (must be resolved first)
+
+The current design keeps the **model key on the VM only**; cluster tasks carry no secrets and have
+restricted egress (verify tasks reach the files host only). Running the proof **model** inside gVisor
+(as OpenCode MCP would) breaks both: the task would hold a model key and need egress to the model
+API host. Two options:
+
+- **A. Scoped key + egress in the cluster (operator-managed).** Inject a spend-limited proof-model
+  key into the proof task (like the existing `gemini-api-secret` slot) and add a per-host egress
+  allowlist for the proof-model API. Keeps the fully-sandboxed agentic authoring the maintainer
+  wants; requires an operator change and widens the cluster's secret/egress surface.
+- **B. Brain on the VM, execution in gVisor (current split preserved).** OpenCode MCP and the proof
+  model run on the VM; only the DAST execution stays in gVisor. No new cluster secret or egress;
+  but the agentic authoring loop is not itself sandboxed.
+
+Recommendation: start with **B** (no trust-domain change, fastest to try the abliterated proof model
+and DSPy loop), and move to **A** only if sandboxing the authoring loop itself proves necessary.
+
+## Security scope (why an abliterated model is in-scope here)
+
+This is authorized **defensive** work: authoring proof-of-concept demos for **known CVE fix-pairs**
+in a **gVisor-isolated** corpus, to demonstrate a regression before push. Guardrails to keep:
+
+- Demos are **data**, not agent code; they stay in the gitignored private area, never echoed.
+- No real-world or third-party live targets; only the frozen fix-pair corpus and owned oracles.
+- gVisor is the execution boundary; the abliterated model never runs code itself, it only writes a
+  declarative demo the trusted verifier executes.
+- The abliterated model is confined to proof-authoring; the search and all reporting stay on the
+  normal models.
+
+## Open questions for the spec
+
+1. A or B for the trust domain (above).
+2. Does the abliterated proof model actually raise the demonstrated rate and remove the wiring
+   misses, measured on the pairs already shown demonstrable (xiaomusic, glance)? Qualify before scaling.
+3. DSPy program shape: what is the proof-authoring signature (inputs: candidate + oracle contract;
+   output: a valid, wired demo), and what metric does it optimize (demonstrated rate at zero false
+   proofs) from OpenObserve traces?
+4. Does OpenCode MCP fit the existing executor/verifier task contract (no-secret, presigned I/O,
+   scratch/egress limits), or does it need a new task kind?
+5. Cost envelope per proof vs the current DeepSeek authoring.
+
+## Not in scope
+
+Changing the search arm, the oracle differential, or the abstract-interpretation triage. This brief
+is only about the **proof-authoring** driver and its learning loop.

.kiro/specs/proof-arm-opencode/spec.json

@@ -0,0 +1,10 @@
+{
+  "feature_name": "proof-arm-opencode",
+  "created_at": "2026-10-07T14:40:00Z",
+  "updated_at": "2026-10-07T14:40:00Z",
+  "language": "en",
+  "phase": "brief",
+  "approvals": {"requirements": {"generated": false, "approved": false}, "design": {"generated": false, "approved": false}, "tasks": {"generated": false, "approved": false}},
+  "ready_for_implementation": false,
+  "summary": "OpenCode-MCP proof-authoring arm for search-with-proof: abliterated/GLM proof model, DSPy-optimized from OpenObserve traces; trust-domain decision (A scoped-key-in-cluster vs B brain-on-VM) must be resolved first. Creds in .env by name."
+}

.kiro/specs/search-with-proof/verification-architecture.md

@@ -0,0 +1,52 @@
+# Search-with-proof: where each stage runs (verification architecture)
+
+Recorded 2026-10-07. search-with-proof has two stages across a trust boundary: a Cairn-inspired
+directed state-space **search**, then a DAST-style **proof (verification)**.
+
+## The two stages
+
+1. **Search (Cairn-inspired).** A blackboard of facts, intents and hints. A reasoner proposes
+   independent, non-overlapping intents; tool-using explorers each confirm one fact against the
+   code. The goal is a declarative demo (a candidate PoC), never proof by itself.
+2. **Proof (DAST verification).** The verifier builds and starts the app, drives the demo's steps
+   through the app's real interface, and watches a verifier-owned canary for a **differential**
+   between the vulnerable and fixed revisions: the owned effect appears on the vulnerable side and
+   not on the fixed side (3/3 vs 0/3). Only this differential earns `demonstrated`.
+
+## Trust boundary — what runs where
+
+The brain runs on the VM; the agent's tool executions and the DAST proof run as isolated tasks in
+the kube-ax cluster. Secrets never enter the cluster.
+
+| Component | Location | Notes |
+|-----------|----------|-------|
+| Coordinator, board, budgets | VM (host) | Orchestrates the search; owns the global budget. |
+| Reasoner + explorer **model calls** | VM (host) | The model key lives only on the VM. This is the brain. |
+| Explorer **tool runs** (`list_files`, `read_file`, `grep`, `run`, build) | kube-ax AX Task (gVisor) | Carry no secrets; inputs/results via presigned object links. |
+| **DAST proof / verification** | kube-ax AX Task (gVisor) | Builds, starts, attacks and observes the app. One task per revision. |
+
+- **gVisor is the isolation boundary.** The proof runs untrusted exploit code against a running
+  app, so it is sandboxed per-task in the cluster.
+- **Secrets stay on the VM.** Executor and verifier tasks carry no credentials; they exchange
+  checkout archives, demos and results through presigned object-store links. Per-host egress is
+  restricted (verify tasks reach the files host only).
+
+## Verification lanes (the `--verify-lane` choice)
+
+- **`ax` (default for paid pilot runs):** verification runs **inside kube-ax** as gVisor AX Tasks,
+  one per side. This is how every paid pilot run this session executed the proof.
+- **`vm` (local):** verification runs in **Bubblewrap on the host**, no cluster. Used for the
+  zero-cost ceiling proofs (a hand-authored demo verified locally with no model and no cluster),
+  which is how glance and xiaomusic were confirmed demonstrable before any spend.
+- **`docker` (replay):** `benchmarks.search.demo_replay` runs a stored demo with no model calls in
+  a local Docker lane.
+
+## Why the proof is dynamic, not abstract interpretation
+
+Abstract interpretation (the static engine and the decision model) is the cheap, generalizable
+**triage/ranker**: it selects and orders candidate regions across any repo without executing. It
+plateaued as a **blocking** gate because it could not prove the required precision. search-with-proof
+is the **dynamic** confirmation: a demonstrated finding is ground truth by execution, so it earns a
+block without calibration. The per-app harness cost (building and running the app, wiring its served
+directory or database to the oracle fixture) is the price of the dynamic proof and is why proof pays
+off where a runnable harness exists, with abstract interpretation remaining the static backbone.