feat(propose-adjudicate-prove): overlay adjudicates inventory before prove

Regex inventory stays the proposer. MAP attaches promote/demote/unadjudicated/coverage
from intra-file taint (tree-sitter when a grammar parses, Python ast as last resort).
Deep sandboxes promotions only, ordered by the existing heuristic ranker plus optional
OpenRouter mechanism recall. The SAST pair slice scores overlay outcomes; the stage-1
detection gate and local pair gate stay inventory-only.

.kiro/specs/propose-adjudicate-prove/brief.md

@@ -0,0 +1,35 @@
+# Brief: regex proposes, semantics adjudicates, sandbox proves
+
+## Problem
+
+OpenUltraSAST already has three scan stages (`quick` inventory, `standard` map, `deep` regression), but **only the first stage actually decides**. Pattern rules propose sinks; the map ranks files; the sandbox can run recipes. Nothing in the middle answers “does this sink receive attacker-controlled data, or is it a Juliet-style good twin / dead assignment / hardcoded command?”
+
+Calibration corpora (cheat-sheet fixtures, OWASP Benchmark true/false files, Juliet `bad`/`good`, CVE pairs) are **nice**: one CWE per file, named sinks, labeled counterparts. Real working trees are not: mixed languages, generated code, unparseable files, framework wrappers, comments, one-hop assignments (`sql = f"…{x}"; cur.execute(sql)`), and no ground-truth labels.
+
+Measured honesty on the labeled SAST slice is about **+9% Youden**. Widening regex to chase that number will fire on every `Runtime.exec` and leak on OWASP-false / Juliet `goodG2B`.
+
+## Approach
+
+Keep three roles, never collapse them:
+
+1. **Propose** — pattern rules + optional SARIF. Stage 1. Does not decide worth-fixing.
+2. **Adjudicate** — tree-sitter IR (multi-language) + taint facts; optional Joern CPG sidecar; Python stdlib parse only as last-resort fallback. Promote, demote, or **unadjudicated**.
+3. **Budget** — ranker + **mechanism memory** (JSONL + OpenRouter embeddings, hard CWE/language/tag filters) **before** prove. Not a verdict. Not TF-IDF. Not raw file-slice embeddings.
+4. **Prove** — sandbox only on promoted, reachable, budgeted candidates.
+
+The primary in-scope target is a **messy working tree the operator is writing**, not a labeled benchmark. Known-vuln corpora remain calibration scoreboards (smoke 90/10, pair Youden, GitHub silent-on-fix). They do not define success on unlabeled code.
+
+## Scope
+
+- Semantic overlay as MAP-stage adjudication; **tree-sitter is the prio engine** (CLI/API, fail-closed). Joern optional. Embeddings tune prove order.
+- Explicit `unadjudicated` when parse or flow fails — do not treat silence as safe.
+- Sandbox prove only after promote.
+- Pair eval scores the overlay on the sast slice; smoke gate stays inventory-only.
+
+## Out of scope
+
+- Replacing pattern rules.
+- LLM as parse/taint engine.
+- Requiring Joern or embeddings for `quick`.
+- Using embedding similarity to silently drop promotions.
+- Auto-writing flow facts from the improve loop.

.kiro/specs/propose-adjudicate-prove/design.md

@@ -0,0 +1,349 @@
+# Design Document
+
+## Overview
+
+**Purpose.** This feature makes the three-stage scan *mean* three jobs: pattern inventory **proposes** sinks; a flow overlay **adjudicates** those proposals on real files; the sandbox **proves** only what was promoted. Operators scanning a working tree they are writing get honest `unadjudicated` instead of fake cleanliness.
+
+**Users.** Developers get `quick` as cheap inventory on WIP code. AppSec gets `standard` dispositions (promote / demote / unadjudicated / coverage). DevOps gets `deep` budget spent on promoted reachable sinks.
+
+**Impact.** Today `quick_scan_findings` is the de facto decision. After this spec, inventory is necessary but not sufficient. MAP writes overlay artifacts. REGRESS candidate selection reads promotions, not demotions.
+
+### Goals
+
+- Map every current scan module onto propose, adjudicate, budget, or prove — rank/embed is not a verdict.
+- Treat messy unlabeled trees as the default; labeled corpora as calibration.
+- Fail closed: cannot parse or cannot follow flow → `unadjudicated`, not demote.
+- **Prioritize the semantic engine now**: tree-sitter IR for in-scope languages; Joern optional CPG sidecar; stdlib Python parse only as last resort.
+- Tunable embeddings + existing ranker order **prove** candidates.
+- SAST pair slice scores the overlay; smoke gate stays inventory-only.
+
+### Non-Goals
+
+- Replacing pattern rules or `LANGUAGE_MANIFESTS`.
+- LLM-as-adjudicator or LLM-as-parser.
+- Requiring Joern or an embedding API for `quick`.
+- Using retrieval similarity to drop promotions.
+- Auto-authoring source/sink/sanitizer facts from `ousast improve`.
+- Buffer-size / memory-safety semantics (Juliet CWE-121 goodG2B stays a known leak until a later spec).
+
+## Boundary Commitments
+
+### This Spec Owns
+
+- Overlay dispositions and flow-fact records.
+- Source / sink / sanitizer **facts as data** (not CWE severity).
+- Tree-sitter probe/runner (CLI-first, like Docker) and last-resort Python stdlib parse.
+- Optional Joern probe/runner (CLI sidecar).
+- Intra-file taint on the tree-sitter IR.
+- Prove-budget: heuristic rank + OpenRouter embeddings over the mechanism log.
+- Calibration scoring of overlay on the sast pair slice; unlabeled-scan honesty.
+
+### Out of Boundary
+
+- Pattern text, rule `enabled|shadow|disabled`, CWE TSV, project score formula (`three-stage-scan` / ruleset / policy).
+- Complexity-map identity keys, Docker sandbox flags, hunter suspicion contract (`three-stage-scan`).
+- Pair catalog schema except scoring **which** findings count (overlay vs inventory).
+- External analyzer execution (SARIF ingest remains a proposal input).
+- MCP exposing `deep`.
+
+### Allowed Dependencies
+
+- Preprocess, mapping, rank (`heuristic_rank` 0.5/0.2/0.3), `quick_scan_findings`, complexity map, `ousast index` / json-local vectorstore, tool hunter, sandbox runner, pair eval, reports.
+- Host binaries when present: `tree-sitter`, `joern` / `joern-parse` (probed, never required for inventory).
+- Optional embedding model from existing `[embeddings]` config.
+- Clearwing as an **oracle** for tree-sitter callgraph + taint-pattern tables + mechanism retrieval — not a dependency.
+
+### Revalidation Triggers
+
+- Adding a fourth disposition that implies “safe.”
+- Demoting when flow is incomplete.
+- Stamping overlay above `static_corroboration`.
+- Selecting sandbox candidates from demoted or unadjudicated sets.
+- Demoting because retrieval score is low.
+- Folding overlay Youden into `python -m openultrasast.gate`.
+- Making tree-sitter or Joern a hard dependency of `quick`.
+
+## Architecture
+
+### Existing Architecture Analysis
+
+Concrete mapping of **what exists today** onto the three roles:
+
+| Role | Stage / mode | Module today | What it actually does | After this spec |
+|------|----------------|--------------|------------------------|-----------------|
+| Propose | STATIC / `quick` | `findings.quick_scan_findings` | Pattern rules decide the report | **Proposal list only** |
+| Propose | STATIC | `mapping.ingest_sarif` | Operator SARIF | Still proposals |
+| Propose | STATIC | `mapping.analyze_entry_points` | Routes / CLI | **Sources** for overlay |
+| Budget | STATIC | `rank.heuristic_rank` 0.5/0.2/0.3 | File budget | Same formula; later **prove order** |
+| Budget | `ousast index` | `vectorstore` json-local | Hunter retrieval | **Prove retrieval** on promotions |
+| Adjudicate? | MAP | `complexity.map` | Hotspot band | Attention only |
+| Adjudicate | MAP | **new** tree-sitter IR + taint | — | **Primary semantic engine** |
+| Adjudicate | MAP | **new** Joern CLI sidecar | — | Optional CPG facts; never required |
+| Adjudicate fallback | MAP | stdlib `ast` | Routes only today | Python last resort if tree-sitter missing |
+| Suspicion | MAP | `tool_hunter` | LLM + grep | May query overlay; never adjudicate |
+| Prove | REGRESS / `deep` | `regress` + sandbox | Recipes on ranked findings | Recipes on **promoted then budgeted** findings |
+| Calibrate | CI | `gate.py` / `pairs` | Cheat-sheet vs Youden | Inventory vs overlay, unchanged split |
+
+**Selected pattern.** Propose → adjudicate → **budget** → prove. Clearwing’s tree-sitter callgraph + taint tables + mechanism memory are the oracle, not a library import. Embeddings never demote.
+
+```mermaid
+flowchart TB
+  subgraph propose["PROPOSE inventory"]
+    PRE[preprocess]
+    EP[entry points as sources]
+    RX[pattern inventory]
+    SARIF[optional SARIF]
+  end
+  subgraph adjudicate["ADJUDICATE overlay"]
+    TS[tree-sitter IR]
+    JOERN[optional Joern CPG]
+    FALLBACK[Python stdlib parse last resort]
+    FACTS[source sink sanitizer facts]
+    TAINT[intra-file taint]
+    DISP[promote demote unadjudicated coverage]
+  end
+  subgraph budget["BUDGET not a verdict"]
+    RANK[heuristic and optional model ranker]
+    VS[json-local embeddings]
+  end
+  subgraph prove["PROVE sandbox"]
+    CAND[promoted reachable then budgeted]
+    BOX[existing Docker runner]
+    VERD[triggerable or not]
+  end
+  PRE --> EP
+  PRE --> RX
+  RX --> DISP
+  SARIF --> DISP
+  EP --> TAINT
+  TS --> TAINT
+  JOERN --> TAINT
+  FALLBACK --> TAINT
+  FACTS --> TAINT
+  TAINT --> DISP
+  DISP --> RANK
+  DISP --> VS
+  RANK --> CAND
+  VS --> CAND
+  CAND --> BOX
+  BOX --> VERD
+```
+
+### Technology Stack
+
+| Layer | Choice | Role |
+|-------|--------|------|
+| CLI / modes | existing `quick` `standard` `deep` | Role gating |
+| Propose | pattern rules + SARIF | Inventory |
+| Semantic IR | `tree-sitter` CLI or API extra; probe like Docker | Primary adjudicator parse |
+| Semantic CPG | Joern CLI when present | Optional inter-file facts |
+| Fallback parse | stdlib `ast` | Python only, last resort |
+| Facts | TOML next to the ruleset | Sources sinks sanitizers |
+| Budget | existing ranker + json-local vectorstore | Prove order, tunable |
+| Prove | existing Docker CLI sandbox | Unchanged runner |
+
+`quick` stays zero-dep. `standard`/`deep` degrade to unadjudicated when parsers are missing.
+
+## File Structure Plan
+
+```
+src/openultrasast/semantic/
+  __init__.py
+  facts.py              # source sink sanitizer facts
+  engines.py            # probe tree-sitter, joern, ast fallback
+  ir.py                 # FileIR from the first engine that works
+  taint.py              # worklist; incomplete -> Unadjudicated
+  overlay.py            # dispositions
+  prove_budget.py       # rank + optional retrieval over promotions
+src/openultrasast/ruleset/semantic/
+  python.toml javascript.toml c.toml java.toml
+```
+
+### Modified Files
+
+- `stages.py` / `cli.py` — overlay in MAP; prove-budget before regress.
+- `findings.py` — inventory unchanged.
+- `regress/candidate.py` — `promote` only, then budget order.
+- `rank.py` / `index.py` / `vectorstore.py` — reuse; do not invent a second store.
+- `reports.py` — disposition columns.
+- `pairs.py` — sast slice uses overlay.
+- `mcp.py` — still no `deep`.
+
+## System Flows
+
+```mermaid
+stateDiagram-v2
+  [*] --> Proposed
+  Proposed --> Unadjudicated: parse fail or flow incomplete or language unsupported
+  Proposed --> Promoted: source reaches sink without sanitizer
+  Proposed --> Demoted: constant or sanitizer dominates
+  Proposed --> Coverage: flow to uninventoried sink
+  Promoted --> Proven: sandbox triggerable
+  Promoted --> Unproven: sandbox skip or unavailable
+  Unadjudicated --> [*]
+  Demoted --> [*]
+  Coverage --> Promoted: same flow rule
+```
+
+**Key decisions**
+
+- Demote only with a positive reason (constant or sanitizer on that path).
+- Unadjudicated is the default for messy real files.
+- Coverage findings enter the same state machine as proposals.
+
+### Unlabeled working-tree flow
+
+No expected.toml. Success is: every inventory item has a disposition; unadjudicated reasons are explicit; `deep` does not execute demoted sinks; `--fail-on worth-fixing` ignores unadjudicated.
+
+## Requirements Traceability
+
+| Requirement | Summary | Components | Flows |
+|-------------|---------|------------|-------|
+| 1.1–1.5 | Role split by mode | Stage plan, overlay, prove budget, regress | propose → adjudicate → budget → prove |
+| 8.1–8.6 | Semantic engines | engines.py, ir.py, taint.py | tree-sitter then Joern then ast |
+| 9.1–9.5 | Prove budget | prove_budget.py, rank, vectorstore | retrieval never demotes |
+| 2.1–2.5 | Messy trees, unadjudicated | IR fail, taint incomplete | unlabeled scan |
+| 3.1–3.5 | Promote demote coverage | taint, overlay | state diagram |
+| 4.1–4.5 | Calibration vs product | gate.py, pairs.py | sast overlay score |
+| 5.1–5.5 | Evidence honesty | overlay evidence, hunter | ladder |
+| 6.1–6.5 | Prove promoted only | candidate filter, sandbox | deep |
+| 7.1–7.5 | Artifacts and fail-on | reports, overlay.json | operator |
+
+## Components and Interfaces
+
+| Component | Domain | Intent | Req Coverage | Dependencies | Contracts |
+|-----------|--------|--------|--------------|--------------|-----------|
+| InventoryProposer | Propose | Existing pattern + SARIF list | 1.1 | findings, mapping | State |
+| FactStore | Adjudicate | Sources sinks sanitizers as data | 3, 5.5 | ruleset/semantic | State |
+| FileIR | Adjudicate | Parse one file or fail | 2.1 | ast | Service |
+| TaintEngine | Adjudicate | Intra-file paths or incomplete | 2.2, 3 | FileIR, FactStore | Service |
+| Overlay | Adjudicate | Dispositions on proposals | 1.2, 3, 5 | TaintEngine | State |
+| ProveFilter | Prove | Candidates from promote | 1.3, 6 | Overlay, regress | Service |
+| OverlayPairEval | Calibrate | SAST slice uses dispositions | 4 | Overlay, pairs | Batch |
+
+### Adjudicate layer
+
+#### OverlayRecord
+
+| Field | Detail |
+|-------|--------|
+| Intent | One disposition per proposal or coverage item |
+| Requirements | 3.5, 7.1 |
+
+**State contract**
+
+```
+proposal_id: str
+path: str
+line: int | None
+disposition: promote | demote | unadjudicated | coverage
+reason: str
+cwe: str
+sources: list[str]
+sinks: list[str]
+sanitizers: list[str]
+evidence_level: static_corroboration | suspicion
+```
+
+**Invariants**
+
+- `demote` requires a recorded constant or sanitizer.
+- `unadjudicated` requires a reason in {`parse_failed`, `language_unsupported`, `flow_incomplete`, `facts_unavailable`}.
+- `promote` and `coverage` do not exceed `static_corroboration`.
+
+#### TaintEngine service
+
+```
+analyze_file(path, text, language, facts) -> FileFlow | Unadjudicated
+adjudicate(proposals, flows, facts) -> list[OverlayRecord]
+```
+
+- Engine order: tree-sitter grammar → Joern file export if probed and useful → Python stdlib parse → unadjudicated.
+- Joern may add paths; it must not demote a tree-sitter promote, and a Joern miss must not demote.
+- Postconditions: every inventory proposal appears exactly once; extras are `coverage` only.
+
+### Prove layer
+
+#### ProveFilter
+
+Inbound: overlay + reachability from mapping. Outbound: existing `regress` candidates.
+
+- Drop `demote`.
+- Do not sandbox `unadjudicated` as a negative proof.
+- Keep `promote` that are reachable or inferred-file-surface.
+- Order survivors with heuristic rank, then **mechanism recall**: hard filter (language, CWE, tags) then OpenRouter dense cosine on the mechanism text. Low similarity never drops a promotion.
+- Write mechanisms only after prove/triggerable. JSONL log is authoritative; json-local `mechanisms` namespace is a rebuildable embedding cache via `OpenRouterEmbeddingClient`.
+
+## Data Models
+
+**Facts (data, versioned with the ruleset)**
+
+- `source`: identifier (e.g. request parameter, header, stdin, argv)
+- `sink`: call shape + CWE (aligned to existing rule ids when possible)
+- `sanitizer`: call shape that stops taint (parameterized execute, `printf` with literal format, `safe_load`, list-form subprocess)
+
+**FileFlow**
+
+- assignments and call arguments in one function
+- one-hop name copies (`bar = param`, `sql = f"...{bar}"`)
+- no types, no inter-file, no may-alias heap in v1
+
+**Mechanism (Clearwing reference architecture)**
+
+Identity is the *pattern*, not a file slice:
+
+| Field | Role |
+|-------|------|
+| id | stable uuid |
+| summary | one sentence, no path/line |
+| cwe, language | filters |
+| tags, keywords | hard filters, not a ranker |
+| what_made_it_exploitable | why a near-miss became a bug |
+| source_finding_id, source_repo | provenance only |
+
+Persistence: append-only JSONL (portable). Recall is **not** Clearwing’s TF-IDF ladder.
+
+1. **Filter** — language, CWE, tags (exact overlap). This is a hard prefilter, not a ranker.  
+2. **Rank** — OpenRouter `/embeddings` (`OpenRouterEmbeddingClient`, existing `[embeddings].model`) over `summary + what_made_it_exploitable + tags`. Cosine against the promotion’s overlay text. Cache vectors in json-local `mechanisms` namespace, keyed by mechanism id + model id.  
+3. **Degrade** — no key / no model / embed failure → heuristic ranker only, degradation recorded. Never bag-of-words cosine.
+
+Query for a promotion: embed the overlay rationale (sources, sink, CWE). Result is a **boost to prove order**, never a demote.
+
+Repo-code chunks (`ousast index` 80-line slices) stay for hunter/verifier retrieval. They are **not** the prove-budget store. Textbook fixtures must not fill the mechanism log unless they were actually proven in the sandbox.
+
+## Error Handling
+
+| Condition | Disposition | Operator sees |
+|-----------|-------------|---------------|
+| Syntax error / parse fail | unadjudicated parse_failed | proposal kept, marked unresolved |
+| No tree-sitter grammar and not Python | unadjudicated language_unsupported | same |
+| Joern missing | ignore sidecar | standard still overlays via tree-sitter |
+| Embedding model missing | heuristic prove order | deep still runs |
+| Callee in another file | unadjudicated flow_incomplete | same |
+| Fact file missing | unadjudicated facts_unavailable; `quick` still emits inventory | degradation in manifest |
+| Sandbox missing | promoted remains unproven | `sandbox_unavailable` |
+
+## Testing Strategy
+
+- Unit: parse fail → unadjudicated; constant `exec("ls")` → demote; `eval(request.args)` → promote; `sql = f"…{x}"; execute(sql)` → coverage or promote.
+- Pair: `--slice sast` uses overlay; `juliet-c-cwe134-printf` stays PASS; `owasp-python-deser` stays PASS; Juliet `goodG2B` exec/strcpy must **demote or unadjudicated**, not inventory-leak counted as pair fail for overlay.
+- Unlabeled: tmp tree with a syntax-error file next to a clean `eval(request.args)` — error file unadjudicated, clean file promoted; no expected.toml required.
+- Gate: `python -m openultrasast.gate` still inventory-only.
+- Deep: candidate list excludes demoted.
+
+## Security
+
+- Overlay does not execute target code.
+- Facts cannot override CWE severity.
+- Hunter still cannot stamp corroboration.
+
+## Performance
+
+- Overlay is per-file, MAP stage, same file budget as rank.
+- Skip files already unreadable at preprocess.
+
+## Migration
+
+- Default `standard` runs overlay when facts load; if facts missing, degrade as Requirement 7.5.
+- Existing `quick` CI unchanged.
+- Pair gate local 100% remains inventory-or-overlay-equivalent on fixture counterparts (those files are still “nice”; unlabeled tests are additional).

.kiro/specs/propose-adjudicate-prove/requirements.md

@@ -0,0 +1,127 @@
+# Requirements Document
+
+## Introduction
+
+OpenUltraSAST users scan **working trees they are writing**: mixed files, incomplete edits, generated code, framework wrappers, and no labels. Today the harness still *decides* with pattern inventory. The complexity map ranks; the sandbox can run; neither adjudicates “this sink is fed by a source” versus “this sink is hardcoded, sanitized, or unreadable.”
+
+This feature splits the scan into three operator-visible roles that must not collapse: **regex proposes, semantics adjudicates, sandbox proves.** Labeled suites (cheat-sheet fixtures, OWASP Benchmark, Juliet, CVE pairs) remain **calibration**. They are not the definition of in-scope code.
+
+## Boundary Context
+
+- **In scope**: Role split on `quick` / `standard` / `deep`; overlay dispositions; tree-sitter (and optional Joern) as the semantic engine; tunable retrieval/rank **before prove**; `unadjudicated` on messy files; sandbox only after promote; calibration vs unlabeled working trees.
+- **Out of scope**: Deleting pattern rules; making an LLM the adjudicator; rewriting CWE policy or project-score formula; requiring Joern or an embedding model for `quick`; auto-generated flow facts from the improve loop; treating benchmark Youden as a merge gate that can unblock a smoke-gate breach. Embedding rank is a **budget**, not a fourth verdict.
+- **Adjacent expectations**: Stage plan, complexity map, Docker sandbox, pair catalog, and 90/10 detection gate from `three-stage-scan` keep their contracts. This spec overlays adjudication on that pipeline; it does not replace stage accounting, sandbox flags, or `LANGUAGE_MANIFESTS`.
+
+## Requirements
+
+### Requirement 1: Three roles stay distinct
+
+**Objective:** As an operator, I want every finding to show whether it is a proposal, an adjudication, or a proof, so that a sink hit is never mistaken for a worth-fixing verdict.
+
+#### Acceptance Criteria
+
+1. When OpenUltraSAST completes a `quick` scan, the system shall emit inventory proposals only and shall not emit adjudication dispositions or sandbox verdicts.
+2. When OpenUltraSAST completes a `standard` scan, the system shall attach an adjudication disposition to each inventory proposal it considered and shall not execute target-derived code to obtain that disposition.
+3. When OpenUltraSAST completes a `deep` scan, the system shall offer sandbox proof only for candidates that adjudication promoted and that remain reachable or inferred-file-surface, ordered by the tunable rank/retrieval budget.
+4. The system shall not treat an inventory proposal as worth-fixing.
+5. The system shall not treat an adjudication promote as crash-reproduced, exploit-demonstrated, or patch-validated.
+
+### Requirement 2: Messy working trees are the primary target
+
+**Objective:** As a developer writing ordinary code, I want the harness to degrade honestly on files that are not labeled benchmarks, so that silence is not reported as safety.
+
+#### Acceptance Criteria
+
+1. When a scanned file is incomplete, generated, minified, or otherwise not interpretable as structured source, the system shall leave matching inventory proposals **unadjudicated** and shall record that reason on the finding.
+2. When no available semantic engine can follow data from a source to a sink for that file (parse failure, missing grammar, cross-file call, dynamic dispatch, or missing callee), the system shall leave the proposal unadjudicated rather than demote it.
+3. When OpenUltraSAST scans a working tree with no benchmark manifest and no expected-finding labels, the system shall still emit proposals, dispositions, and (in `deep`) proofs without requiring a counterpart “fixed” tree.
+4. If the operator reads a report for an unadjudicated proposal, then the system shall present it as unresolved inventory, not as a verified vulnerability and not as a cleared finding.
+5. The system shall not require a file to resemble an OWASP Benchmark or Juliet test case in order to produce a proposal.
+
+### Requirement 3: Adjudication promote, demote, coverage
+
+**Objective:** As an AppSec reviewer, I want the overlay to keep, drop, or add findings based on flow, so that hardcoded and sanitized sinks stop looking like attacks.
+
+#### Acceptance Criteria
+
+1. When a proposal’s sink is reachable from an identified untrusted source without an identified sanitizer in the adjudicated region, the system shall **promote** the proposal.
+2. When a proposal’s sink is fed only by a constant, a sanitizer, or an identified non-attacker source in the adjudicated region, the system shall **demote** the proposal and shall not list it as a promoted finding.
+3. When adjudication finds an untrusted source flowing to a dangerous sink that inventory did not propose, the system shall emit a **coverage** finding at corroboration-or-lower evidence, tagged as overlay-originated.
+4. When both a source-to-sink path and a sanitizer appear to apply, the system shall not promote unless the sanitizer does not dominate that path.
+5. The system shall persist promote, demote, unadjudicated, and coverage outcomes in the scan artifacts with the proposal identifier they refer to.
+
+### Requirement 4: Calibration corpora do not define product success
+
+**Objective:** As a maintainer, I want labeled suites to measure the overlay without becoming the only in-scope code, so that we do not overfit textbook cases.
+
+#### Acceptance Criteria
+
+1. When the stage-1 detection gate runs, the system shall score inventory only on the existing cheat-sheet corpus and shall not fold overlay Youden or unlabeled-scan counts into that gate.
+2. When the pair-efficiency evaluation runs on the SAST slice, the system shall score **adjudicated** outcomes (promote on the vulnerable side, demote or silent on the false or good side), not raw inventory hits.
+3. When overlay changes raise SAST Youden and also cause the stage-1 detection gate to fail, the system shall treat the detection-gate failure as blocking.
+4. The system shall keep labeled pair fixtures and SAST-slice cases out of the stage-1 cheat-sheet corpus map.
+5. The system shall not require a labeled counterpart tree in order to scan an operator working tree.
+
+### Requirement 5: Evidence and models stay honest
+
+**Objective:** As a reviewer, I want overlay and hunter output to stay on the evidence ladder, so that a model cannot mint proof.
+
+#### Acceptance Criteria
+
+1. The system shall keep inventory and successful intra-file adjudication at `static_corroboration` or below.
+2. When the tool hunter emits a finding, the system shall keep that finding at `suspicion` unless an independent corroborating stage has already raised it.
+3. If an overlay or hunter result claims an evidence level above corroboration without a sandbox or verifier step that earned it, then the system shall reject that claim.
+4. The system shall not use a language model as the adjudication engine that decides promote or demote.
+5. Where CWE policy applies, the system shall resolve severity from the central CWE policy, not from the overlay or the proposing rule’s private severity string.
+
+### Requirement 6: Sandbox proves only promoted work
+
+**Objective:** As a DevOps engineer, I want isolation to spend budget on promoted sinks, so that `deep` does not execute every regex hit.
+
+#### Acceptance Criteria
+
+1. When `deep` runs and the sandbox is available, the system shall select regression candidates from promoted findings, not from demoted findings.
+2. When a finding is unadjudicated, the system shall not treat a sandbox skip as proof that the finding is safe.
+3. If the sandbox is unavailable, then the system shall keep promoted findings as unproven corroboration, record `sandbox_unavailable`, and shall not invent a worth-fixing verdict.
+4. When sandbox proof is `triggerable` on a promoted reachable finding, the system shall allow `worth_fixing` to follow the existing worth-fixing rule from the three-stage scan.
+5. The system shall not execute target-derived code outside the existing isolated sandbox path.
+
+### Requirement 7: Operator-visible artifacts and fail-on
+
+**Objective:** As an operator, I want the report to show the three-role pipeline on real trees, so that I can act on promoted and worth-fixing items without trusting unlabeled silence.
+
+#### Acceptance Criteria
+
+1. When a `standard` or `deep` scan finishes, the system shall write overlay artifacts that list each considered proposal, its disposition, and any flow facts or unadjudicated reason.
+2. When the markdown or SARIF report is written, the system shall distinguish promoted, demoted, unadjudicated, and coverage items.
+3. Where `--fail-on worth-fixing` is used, the system shall fail only on worth-fixing as already defined, not on unadjudicated inventory.
+4. The system shall keep `quick` usable without overlay configuration and without a model.
+5. If overlay fact data is missing or invalid, then the system shall degrade to inventory-only for that scan, mark proposals unadjudicated with that reason, and shall not abort `quick`.
+
+### Requirement 8: Semantic engines are multi-language and optional-at-runtime
+
+**Objective:** As an AppSec engineer scanning mixed-language trees, I want adjudication to use a real parser family, so that Python-only stdlib parsing is not the product engine.
+
+#### Acceptance Criteria
+
+1. When a tree-sitter grammar for the file’s language is available, the system shall use that parse as the primary intra-file IR for adjudication.
+2. When tree-sitter is unavailable for that language, the system shall try a stdlib parse only for Python and shall otherwise leave the proposal unadjudicated with language_unsupported or parse_failed.
+3. Where Joern is installed and the language is one Joern can export, the system shall be allowed to attach Joern flow facts as **additional** corroboration; Joern absence shall not fail `quick` or `standard`.
+4. If Joern and tree-sitter disagree or Joern returns incomplete paths, then the system shall not demote on that disagreement; it shall promote only on a complete dominating path or leave the item unadjudicated.
+5. The system shall not require Joern or tree-sitter to be present for a `quick` inventory scan.
+6. The system shall not use a language model as the parse or taint engine.
+
+### Requirement 9: Mechanism memory ranks prove budget, not truth
+
+**Objective:** As an operator on a large messy tree, I want proven-bug *mechanisms* (not raw file slices) to decide **what to prove next**, so that the sandbox follows patterns that have worked on real bugs.
+
+#### Acceptance Criteria
+
+1. When `deep` has more promoted candidates than the sandbox budget, the system shall order them using the existing ranker axes plus OpenRouter embedding similarity over mechanism records, after hard filters on language, CWE, and tags.
+2. When no embedding model or API key is configured, the system shall order candidates with the heuristic ranker only, record that degradation, and shall not skip prove.
+3. The system shall not demote or drop a promotion solely because mechanism similarity is low.
+4. When the embedding index is missing or stale, the system shall rebuild it from the mechanism log via OpenRouter embeddings; if that rebuild fails, the system shall record the degradation and continue on heuristic order.
+5. The system shall keep hard filters operator-tunable (language, CWE, tags) without changing CWE severity policy.
+6. When a finding is sandbox-proven triggerable (or otherwise verified at corroboration-or-higher with a prove step), the system shall append an abstract mechanism record to the mechanism log: summary, CWE, language, tags, what made it exploitable — without file:line as the identity.
+7. The system shall treat the append-only mechanism log as the source of truth; any vector index shall be a rebuildable cache of that log.
+8. The system shall not persist mechanisms from inventory-only, demoted, or unadjudicated proposals.

.kiro/specs/propose-adjudicate-prove/research.md

@@ -0,0 +1,105 @@
+# Research & Design Decisions
+
+## Summary
+
+- **Feature**: `propose-adjudicate-prove`
+- **Discovery Scope**: Extension of `three-stage-scan` (MAP grows an overlay; STATIC and REGRESS stay)
+- **Key Findings**:
+  - Inventory already decides; MAP ranks; REGRESS can run. Nothing adjudicates flow.
+  - Labeled SAST slice Youden is about +9%. Leaks are OWASP-false / Juliet `goodG2B` that still contain the sink. Misses are one-hop assignments and sink aliases.
+  - Clearwing already does the split we want: tree-sitter callgraph + pattern taint tables, then ranker (surface/influence/reachability 0.5/0.2/0.3), then mechanism-memory embeddings. OpenUltraSAST already copied the rank formula and has `json-local` vectors; they are not wired as prove-budget.
+- Tree-sitter CLI/API covers C/C++/Python/JS/Go/Rust (Clearwing grammars); Joern is the CPG sidecar when present. Stdlib `ast` is last-resort Python only. LLM hunter remains suspicion-only.
+  - Real working trees will often fail parse or cross a file boundary. Those cases must stay **unadjudicated**, not demoted.
+
+## Research Log
+
+### Labeled vs unlabeled code
+
+- **Context**: Operator: known-vuln corpora are “nice”; written code will not be.
+- **Sources Consulted**: In-tree `LANGUAGE_MANIFESTS`, `benchmarks/pairs/`, OWASP Benchmark true/false files, Juliet `bad`/`goodG2B`/`goodB2G`, CWE-Bench-Java catalog.
+- **Findings**:
+  - Cheat-sheets: one CWE, named sink, often same-line source.
+  - OWASP: true and false files both often contain `exec` / `eval`; the difference is source constancy or infeasible branches.
+  - Juliet `goodG2B`: hardcoded source, **same sink**.
+  - Juliet `goodB2G`: same source, **sanitized sink** (`printf("%s")`).
+  - Working trees: syntax errors, generated bundles, wrappers (`helpers.db_sqlite.execute`), no labels.
+- **Implications**: Overlay scored on sast slice; unlabeled scans must not pretend demote. Unadjudicated is a first-class disposition.
+
+### Engine choice
+
+- **Context**: Operator prefers tree-sitter + Joern look, embeddings before prove, still v1-focused.
+- **Sources Consulted**: `clearwing/sourcehunt/callgraph.py`, `taint.py`, `ranker.py`, `mechanism_memory.py`; `openultrasast/rank.py`, `vectorstore.py`, `index.py`.
+- **Findings**:
+  - Clearwing tree-sitter is optional: missing grammar disables callgraph, does not crash.
+  - Clearwing taint is intra-procedural, pattern tables for sources/sinks — same shape as our fact TOML.
+  - Clearwing ranker fills reachability from the callgraph; taint_paths boost surface. Embeddings retrieve *mechanisms*, they do not decide taint.
+  - Our `heuristic_rank` already uses surface·0.5 + influence·0.2 + reachability·0.3. Vector store bakeoff selected `json-local`. `VALID_NAMESPACES` already includes `mechanisms` but nothing writes Clearwing-style records into it.
+
+### Clearwing vector-store reference (real-world bugs)
+
+- **Context**: Operator: Clearwing’s store is effective on real bugs, not textbook files.
+- **Sources Consulted**: `clearwing/sourcehunt/mechanism_memory.py`, `data/memory/semantic_memory.py`, `docs/architecture.md` steps 7–8; `openultrasast/index.py` namespaces.
+- **Findings**:
+  - Store **mechanisms**, not findings and not 80-line file windows. Example: “length field trusted before alloc; 16-bit value widened to size_t.”
+  - JSONL is the source of truth (`~/.clearwing/sourcehunt/mechanisms.jsonl`). Chroma/sqlite embeddings are ephemeral caches rebuilt from JSONL.
+  - Write path is **verified findings only** (after adversarial verify / crash). Suspicion never seeds the store.
+  - Clearwing’s JSONL + verified-write + metadata filters are the reference. Its TF-IDF default is **not**: bag-of-words will not match paraphrased real bugs (`length field trusted before alloc` vs `user-controlled size_t in malloc`).
+  - OpenUltraSAST already has `OpenRouterEmbeddingClient` and json-local cosine. Use that as the only semantic ranker; CWE/language/tags are hard filters. No TF-IDF, no Chroma, no local MiniLM.
+  - Query is language + file tags + optional free text; same-language boost +0.5. Top-N injects hunter context and variant-grep seeds — it does not decide taint.
+  - Variant loop then greps the *messy* tree for structural matches of that mechanism. That is how it leaves Juliet behind.
+- **Implications**: Copy JSONL + verified-write + metadata filters. Rank with OpenRouter embeddings only. Do not copy TF-IDF. Do not embed 80-line file windows as the prove store. Seed from sandbox-proven mechanisms, not OWASP `BenchmarkTest00007`.
+  - Joern CLI (`joern-parse` / scripts) is the only practical CPG without a Scala runtime in-process.
+- **Implications**: Probe tree-sitter like Docker. Joern sidecar cannot demote. Embeddings order prove only.
+
+### Decision: Python intra-file first
+
+- **Context**: Zero-dep core vs multi-language trees.
+- **Selected**: **Superseded.** Tree-sitter is the prio engine; stdlib `ast` is Python last resort; `quick` stays zero-dep.
+- **Rationale**: Operator working trees are mixed-language; Python-only adjudication would leave JS/C/Java as perpetual unadjudicated.
+- **Trade-offs**: `standard` needs a grammar or CLI on PATH; missing tools → unadjudicated, not skip the scan.
+
+### Evidence ladder
+
+- **Context**: Three-stage-scan forbids hunter JSON as corroboration.
+- **Sources Consulted**: `verification.EvidenceLevel`, `tool_hunter` suspicion rule, `worth_fixing` gate.
+- **Findings**: Overlay can justify promote at `static_corroboration`. It cannot skip to crash or exploit. Worth-fixing stays sandbox + reachability.
+- **Implications**: Disposition is not an evidence rung. Do not add a seventh ladder value.
+
+## Architecture Pattern Evaluation
+
+| Option | Description | Strengths | Risks | Notes |
+|--------|-------------|-----------|-------|-------|
+| Replace regex with CodeQL | External engine is the detector | Real dataflow | Breaks zero-dep, smoke gate, ledger shadows | Rejected |
+| LLM hunter as adjudicator | Model reads file and votes | Flexible on messy code | Unstable Youden; violates suspicion rule | Rejected |
+| Overlay on inventory | Regex proposes; tree-sitter taint adjudicates; embed ranks prove | Fits stages; multi-lang | Parser must be probed | **Selected** |
+| Whole-program taint v1 | Inter-file | Closes wrappers | Too large; false demote risk | Defer; stay unadjudicated |
+
+## Design Decisions
+
+### Decision: Unadjudicated is not demote
+
+- **Context**: Messy files and cross-file flow.
+- **Alternatives**: Silent drop; treat as safe; force demote.
+- **Selected**: Explicit `unadjudicated` with reason.
+- **Rationale**: Operator writing code must not read silence as “clean.”
+- **Trade-offs**: Reports stay noisy until languages and inter-file land.
+- **Follow-up**: Count unadjudicated rate on unlabeled trees as an honesty metric.
+
+### Decision: Score overlay on sast slice, inventory on smoke gate
+
+- **Context**: +9% Youden vs 93% cheat-sheet recall.
+- **Selected**: Two gates stay separate; overlay Youden cannot unblock smoke failure.
+- **Rationale**: Same as detection-gate vs score in the improve loop.
+
+## Risks & Mitigations
+
+- False demote on real bugs (infeasible-branch OWASP tricks, wrappers) — never demote when flow is incomplete; only demote when the engine *has* a dominating constant or sanitizer.
+- Youden chase via extra sinks — each coverage rule needs a false/good counterpart that must stay demoted or silent.
+- Parse failures on operator WIP — unadjudicated, `quick` still works.
+
+## References
+
+- `.kiro/specs/three-stage-scan/design.md` — stage plan, sandbox, hunter suspicion
+- `benchmarks/pairs/sast/README.md` — OWASP/Juliet slice
+- NIST Juliet `goodG2B` vs `goodB2G` templates
+- OWASP Benchmark expectedresults true/false protocol

.kiro/specs/propose-adjudicate-prove/spec.json

@@ -0,0 +1,22 @@
+{
+  "feature_name": "propose-adjudicate-prove",
+  "created_at": "2026-09-04T10:58:28Z",
+  "updated_at": "2026-09-04T12:00:00Z",
+  "language": "en",
+  "phase": "implementation",
+  "approvals": {
+    "requirements": {
+      "generated": true,
+      "approved": true
+    },
+    "design": {
+      "generated": true,
+      "approved": true
+    },
+    "tasks": {
+      "generated": true,
+      "approved": true
+    }
+  },
+  "ready_for_implementation": true
+}

.kiro/specs/propose-adjudicate-prove/tasks.md

@@ -0,0 +1,142 @@
+# Implementation Plan
+
+- [x] 1. Foundation: overlay vocabulary and fact data
+- [x] 1.1 Define overlay records and fail-closed reasons
+  - Dispositions are promote, demote, unadjudicated, coverage only.
+  - Unadjudicated reasons are parse_failed, language_unsupported, flow_incomplete, facts_unavailable.
+  - Demote is illegal without a recorded constant or sanitizer in the record.
+  - Tests construct records and reject demote-without-reason.
+  - Observable: a unit test fails if a demote record omits the dominating fact.
+  - _Requirements: 3.5, 2.1, 2.2, 5.1_
+  - _Boundary: OverlayRecord_
+
+- [x] 1.2 (P) Load source, sink, and sanitizer facts as versioned data
+  - Facts bind to CWE ids that already exist in policy.
+  - Invalid or missing fact files yield facts_unavailable, not a crash of `quick`.
+  - Observable: loading a broken fact file returns a structured error the overlay can attach to every proposal.
+  - _Requirements: 5.5, 7.5_
+  - _Boundary: FactStore_
+
+- [x] 2. Semantic engines: tree-sitter first
+- [x] 2.1 Probe tree-sitter like Docker and parse in-scope languages
+  - Primary IR comes from tree-sitter when a grammar exists (Python, JS, C/C++, Java if present).
+  - Missing CLI or grammar does not crash `quick`; those files become unadjudicated.
+  - Stdlib Python parse is last resort only when tree-sitter is absent.
+  - Observable: a JS `eval(req.query.x)` file yields IR when tree-sitter JS is available, and language_unsupported when it is not.
+  - _Requirements: 8.1, 8.2, 8.5, 8.6, 2.1_
+  - _Boundary: FileIR_
+  - _Depends: 1.1_
+
+- [x] 2.2 (P) Probe Joern as an optional CPG sidecar
+  - Joern facts may add paths; Joern missing or incomplete must not demote.
+  - `quick` and `standard` succeed without Joern.
+  - Observable: with Joern absent, overlay still runs; a Joern-only miss does not turn a tree-sitter promote into demote.
+  - _Requirements: 8.3, 8.4, 8.5_
+  - _Boundary: JoernSidecar_
+
+- [x] 2.3 Follow one-hop assignments and call arguments on the IR
+  - Cover `bar = param`, f-string or concat into `sql`, then `execute(sql)`, in Python and the equivalent JS/C patterns the facts describe.
+  - Incomplete callees mark flow_incomplete, not safe.
+  - Observable: split-sink Python fixture yields a source-to-sink path; a call into a missing module does not.
+  - _Requirements: 2.2, 3.1, 3.4, 2.5_
+  - _Boundary: TaintEngine_
+  - _Depends: 2.1, 1.2_
+
+- [x] 3. Adjudicate inventory proposals
+- [x] 3.1 Promote, demote, and leave unadjudicated
+  - Every inventory proposal for a considered file appears exactly once.
+  - `eval(request.args)` promotes; `eval("1")` demotes; unreadable file stays unadjudicated.
+  - Observable: overlay output length equals proposal count for that file, plus coverage items only.
+  - _Requirements: 1.2, 3.1, 3.2, 2.4, 3.5_
+  - _Boundary: Overlay_
+  - _Depends: 2.3_
+
+- [x] 3.2 Emit coverage findings for uninventoried sinks with flow
+  - Coverage stays at corroboration or below and is tagged overlay-originated.
+  - No coverage item is stamped as worth-fixing or sandbox-proven.
+  - Observable: `hashlib.new('md5')` with tainted input appears as coverage when facts include that sink and inventory missed it.
+  - _Requirements: 3.3, 1.4, 1.5, 5.1_
+  - _Boundary: Overlay_
+
+- [x] 4. Integration: stages, prove filter, reports
+- [x] 4.1 Run overlay in standard, not in quick
+  - `quick` artifacts contain no dispositions.
+  - `standard` attaches a disposition to each considered proposal without executing target code.
+  - Observable: a `quick` run on a tiny tree has no overlay file; `standard` writes overlay artifacts.
+  - _Requirements: 1.1, 1.2, 7.1, 7.4_
+  - _Boundary: StagePlan, Overlay_
+  - _Depends: 3.1_
+
+- [x] 4.2 Select deep candidates from promotions only
+  - Demoted findings are absent from the sandbox candidate list.
+  - Unadjudicated findings are not used as negative proof when the sandbox is skipped.
+  - Sandbox unavailable keeps promoted items unproven and records sandbox_unavailable.
+  - Order remaining promotions with the heuristic ranker; if embeddings are configured, retrieval may reorder but must not drop.
+  - Observable: a tree with one demoted `exec("ls")` and one promoted `eval(request.args)` offers only the latter to regression when Docker is probed; with embeddings off, heuristic order is used.
+  - _Requirements: 1.3, 6.1, 6.2, 6.3, 6.4, 6.5, 9.1, 9.2, 9.3, 9.4, 9.5_
+  - _Boundary: ProveFilter_
+  - _Depends: 4.1_
+
+- [x] 4.3 Distinguish dispositions in markdown and SARIF
+  - Promoted, demoted, unadjudicated, and coverage are visible without reading JSON.
+  - `--fail-on worth-fixing` does not fail on unadjudicated inventory.
+  - Observable: report.md contains the four labels; fail-on worth-fixing on an unadjudicated-only tree exits 0.
+  - _Requirements: 7.2, 7.3, 2.4_
+  - _Boundary: Reports_
+  - _Depends: 4.1_
+
+- [x] 4.4 Mechanism memory with OpenRouter embeddings as the only semantic ranker
+  - Append-only mechanism log is source of truth; json-local `mechanisms` namespace is a rebuildable OpenRouter vector cache.
+  - Hard-filter by language, CWE, tags; rank remaining by OpenRouter cosine on mechanism text vs promotion overlay text.
+  - No TF-IDF. Missing key or embed failure → heuristic order plus a recorded degradation; prove still runs.
+  - Write mechanisms only from sandbox-proven findings; never from unadjudicated inventory.
+  - Observable: after one triggerable finding, a paraphrased second promotion ranks above an unrelated CWE; with OPENROUTER_API_KEY unset, both remain candidates in heuristic order.
+  - _Requirements: 9.1, 9.2, 9.3, 9.4, 9.5, 9.6, 9.7, 9.8_
+  - _Boundary: ProveBudget_
+  - _Depends: 4.2_
+
+- [x] 5. Evidence honesty
+- [x] 5.1 Keep hunter and overlay off the proof rungs
+  - Overlay promote remains static_corroboration or below.
+  - Hunter output remains suspicion unless an independent stage already raised it.
+  - A fixture that tries to stamp overlay as exploit_demonstrated is rejected.
+  - Observable: existing hunter suspicion tests still pass; overlay records never contain crash_reproduced or higher.
+  - _Requirements: 5.1, 5.2, 5.3, 5.4_
+  - _Boundary: Overlay, ToolHunter_
+  - _Depends: 3.1_
+
+- [x] 6. Calibration vs unlabeled product
+- [x] 6.1 Score the sast pair slice on overlay outcomes
+  - Vulnerable side counts promote; false or good side counts demote or silent promoted-empty.
+  - Stage-1 detection gate still uses inventory on cheat-sheet manifests only.
+  - Overlay Youden cannot mark a failed detection gate as passed.
+  - Sast and pair fixtures remain outside LANGUAGE_MANIFESTS.
+  - Observable: `ousast pairs --slice sast` changes when overlay demotes Juliet goodG2B exec; `python -m openultrasast.gate` still ignores that slice.
+  - _Requirements: 4.1, 4.2, 4.3, 4.4_
+  - _Boundary: OverlayPairEval_
+  - _Depends: 3.1, 4.1_
+
+- [x] 6.2 Scan an unlabeled messy tree without expected findings
+  - A syntax-broken file next to a clear request-to-eval file: broken file unadjudicated, eval promoted.
+  - No counterpart fixed tree and no manifest required.
+  - Observable: `ousast scan` on that tmp tree writes both dispositions.
+  - _Requirements: 2.3, 2.5, 4.5, 7.4_
+  - _Boundary: Overlay_
+  - _Depends: 4.1_
+
+- [x] 7. End-to-end validation
+- [x] 7.1 Regression of three-stage contracts
+  - Quick still has no model and no target execution.
+  - Deep still does not run outside the existing sandbox.
+  - MCP still rejects deep.
+  - Observable: existing three-stage-scan tests for modes, sandbox, and MCP remain green.
+  - _Requirements: 1.1, 6.5, 7.4_
+  - _Depends: 4.2, 5.1_
+
+## Implementation Notes
+
+- Python adjudication uses stdlib `ast` when tree-sitter has no grammar; JS/C/Java stay `language_unsupported` until a grammar actually parses.
+- Pair eval on the sast slice uses overlay when at least one promote/demote/coverage exists; otherwise it falls back to inventory so C/Java Juliet cases do not collapse without grammars.
+- Intra-file taint is one-hop names plus source patterns in expressions. Heap channels (ConfigParser get/set) stay `flow_incomplete`.
+- OpenRouter embeddings reorder promotions only; missing key records `embeddings_unavailable` and prove still runs.
+- Hunter findings stay off the sandbox candidate list; only overlay promotions are proven.