spec(search-with-proof): brief and requirements for review

After reviewing Cairn: detection so far classified excerpts and hit a precision
wall; this adds directed search with an objective goal (a re-verified
demonstration), a fact/intent board, and reason/explore steps as AX Tasks on
kube-ax. Design only learns from Cairn (AGPL); no code copied.

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

.kiro/specs/search-with-proof/brief.md

@@ -0,0 +1,40 @@
+# Brief: search with proof
+
+Maintainer, 2026-10-05, after reviewing Cairn (github.com/oritera/Cairn): "we are still not progressing through the
+state space search / not finding what we need and the progress is sort of slow ... i think something is missing."
+And: "I'd move to primarily executing in the cluster."
+
+## What was missing
+
+Every detection step so far classifies: it scores one function excerpt and then tries to make the score precise
+enough to block. Calibration, Wilson bounds, pooled block gates, prompt variants and trained models all hit the same
+wall: ranking is decent (within-pair AUC about 0.76), but precision at the top cannot be proven to 95% on our data.
+
+Cairn treats a security problem as a directed search with an objectively checkable goal. A shared board holds
+confirmed facts, open intents and human hints. A reasoner proposes independent intents; explorers with real tools
+each confirm one fact; the loop ends when the goal is demonstrably met.
+
+Three things follow for OpenUltraSAST:
+
+1. **An objective success condition.** A finding is demonstrated when a test or proof of concept fails on the
+   vulnerable code and passes on the fixed code (or, for a push, fails on head and passes on base where applicable).
+   A demonstrated finding is right by construction; it needs no calibration and no training data, so it generalises
+   to unseen repositories by construction.
+2. **Exploration with tools.** Agents that read other files, follow callers, build and run the code, instead of a
+   single-shot judgement of one excerpt.
+3. **Search state per repository and push.** Facts and intents accumulate on a board instead of every question
+   starting from zero.
+
+## Shape
+
+- The cheap layers (quick rules, engine, classifier) become triage: they rank candidates.
+- Agentic search runs only on the top-ranked candidates of a push, under a per-push budget.
+- BLOCK only on a demonstrated finding. Advisory for plausible, unproven ones. "Could not demonstrate" is recorded as
+  such, never as "not vulnerable".
+- Execution is primarily in the kube-ax cluster: reason and explore steps are AX Tasks; the VM coordinates.
+- Model access: a scoped, budget-limited key in the cluster, managed by the operator.
+
+## Not in scope
+
+Copying Cairn code (AGPL-3.0; this repository is Apache-2.0). Offensive use against systems we do not own: all
+execution is against code under analysis, inside gVisor sandboxes.

.kiro/specs/search-with-proof/requirements.md

@@ -0,0 +1,103 @@
+# Requirements Document
+
+## Introduction
+
+Add a search-with-proof stage: for the top-ranked candidates of a push or a labelled pair, sandboxed tool-using agents
+search for a demonstration of the vulnerability, coordinated through a fact/intent board, executing primarily in the
+kube-ax cluster. BLOCK becomes "demonstrated", not "scored above a threshold". Context: `brief.md`, roadmap G1-G2,
+`unseen-repo-evaluation` (the pool and metric this arm is judged by).
+
+## Boundary Context
+
+- **In scope**: the board (facts, intents, hints) in the memory store; reason and explore steps as AX Tasks; the
+  demonstration contract and its verification; triage-to-search budgeting; a pilot on known fix pairs; a G1 arm on the
+  unseen pool; model access through an operator-managed scoped key.
+- **Out of scope**: copying Cairn code (AGPL-3.0); network actions against anything but the code under analysis;
+  changing the existing quick rules, engine or classifier (they are inputs here).
+- **Adjacent expectations**: `unseen-repo-evaluation` scores this arm; the AX batch dispatcher (`benchmarks/ax/batch.py`)
+  and the kube-ax constraints (2 heavy lanes, `ousast-engine-` names, egress to public HTTPS) apply;
+  `learned-decision-engine` Req 6.4 BLOCK rule is superseded for this arm by "demonstrated".
+
+## Requirements
+
+### Requirement 1: The board
+
+**User Story:** As the maintainer, I want each search to keep its state, so exploration builds on what is already
+known instead of restarting.
+
+#### Acceptance Criteria
+
+1. Per search (one candidate or one push), the board holds facts (confirmed, objective, with the evidence that
+   confirmed them), intents (declared directions, open or concluded, with the facts they start from) and hints (human
+   input, absorbed on the next read).
+2. The board lives in the memory store, versioned, and every fact and intent carries the step and the task that wrote
+   it.
+3. A search ends when a fact meets the goal (Requirement 3), when its budget is spent, or when the reasoner proposes no
+   new intent and none is open; the end reason is recorded.
+
+### Requirement 2: Reason and explore steps
+
+**User Story:** As the maintainer, I want the search driven by the board's state, not by fixed roles.
+
+#### Acceptance Criteria
+
+1. A reason step reads the board and returns: the goal is met (citing facts), or at most N new, independent,
+   non-overlapping intents, or no new intent.
+2. An explore step claims one intent, works it with tools inside the sandbox (read files, search the repository,
+   follow callers, build, run tests and scripts against the code under analysis), and returns exactly one new fact or
+   a recorded failure.
+3. Both run as AX Tasks in the kube-ax cluster by default; the VM coordinates (board, dispatch, budgets) and is a
+   fallback lane only.
+4. Parallel explores of one search never race on the board (claims as in the batch dispatcher).
+
+### Requirement 3: The demonstration contract
+
+**User Story:** As the maintainer, I want BLOCK to mean "shown", so precision does not depend on calibration.
+
+#### Acceptance Criteria
+
+1. A demonstration is an executable artefact (test, script or request sequence) that the system, not the agent,
+   re-runs in a fresh sandbox: it fails (shows the vulnerable behaviour) on the vulnerable revision and passes on the
+   fixed revision for a labelled pair; for a push it shows the behaviour on head (and not on base where the change
+   introduced it).
+2. Only a re-verified demonstration counts as a demonstrated finding. The agent's own claim of success is never enough.
+3. Outcomes are recorded as `demonstrated`, `plausible_unproven` (evidence but no passing demonstration),
+   `could_not_build` / `could_not_run` (environment failures), or `no_evidence`; none of the failure outcomes is ever
+   reported as "not vulnerable".
+
+### Requirement 4: Triage and budget
+
+**User Story:** As the maintainer, I want search spent where it matters, at a known cost.
+
+#### Acceptance Criteria
+
+1. Candidates come from the existing layers (quick rules, engine, classifier scores); only the top K per push or per
+   pair side are searched; K and the per-search and per-push budgets (model spend, task count, wall time) are
+   configuration, enforced by the coordinator.
+2. Every search records its model spend, task count and wall time; a budget is never exceeded.
+3. Paid runs need the maintainer's budget go-ahead with a ceiling, as all paid steps do.
+
+### Requirement 5: Model access in the cluster
+
+**User Story:** As the maintainer, I want agents in the cluster to reach a model without spreading keys.
+
+#### Acceptance Criteria
+
+1. The agents' model key is a scoped, budget-limited key provided by the operator inside the cluster (AX v0.3.1
+   injects only `gemini-api-secret` as `GEMINI_API_KEY`; the design names the exact mechanism agreed with the
+   operator). Store credentials stay out of the cluster (presigned links, as today).
+2. The key never appears in a manifest, a log, a board entry or a record.
+
+### Requirement 6: Pilot, then the unseen pool
+
+**User Story:** As the maintainer, I want to know quickly whether search with proof works before scaling it.
+
+#### Acceptance Criteria
+
+1. Pilot: about 20 known fix pairs across families and languages; for each, search runs on the vulnerable side and
+   on the fixed side under the same budget. Reported: demonstrated rate on vulnerable sides, any demonstration on a
+   fixed side (a false proof, which must be zero), environment-failure rate, spend and wall time per search.
+2. Exit of the pilot: at least one family with demonstrations on vulnerable sides and zero false proofs; otherwise
+   the result is recorded and the arm is not scaled.
+3. Then a registered G1 arm on the unseen-repo pool: catch rate at the pool's false-alarm budgets, with BLOCK only on
+   demonstrated findings, compared with the classifier arms.

.kiro/specs/search-with-proof/spec.json

@@ -0,0 +1,13 @@
+{
+  "feature_name": "search-with-proof",
+  "created_at": "2026-10-05T12:00:00Z",
+  "updated_at": "2026-10-05T12:00:00Z",
+  "language": "en",
+  "phase": "requirements-generated",
+  "approvals": {
+    "requirements": {"generated": true, "approved": false},
+    "design": {"generated": false, "approved": false},
+    "tasks": {"generated": false, "approved": false}
+  },
+  "ready_for_implementation": false
+}