fix: V-model pilot — scaffold scripts/vmodel/ + close 9 of 12 rivet validate errors

artifacts/stpa/attack-scenarios.yaml

@@ -917,6 +917,10 @@ artifacts:
       - type: executed-by
         target: TA-1
 
+      - type: exploits
+        target: UCA-36
+      - type: exploits
+        target: DF-19
   - id: AS-35
     type: attack-scenario
     title: PATH injection during build environment attestation
@@ -948,6 +952,8 @@ artifacts:
       - type: executed-by
         target: TA-3
 
+      - type: exploits
+        target: UCA-34
   - id: AS-37
     type: attack-scenario
     title: Cert-chain downgrade via silently-swallowed cert_count parse error
@@ -1028,3 +1034,7 @@ artifacts:
         target: H-14
       - type: executed-by
         target: TA-3
+      - type: exploits
+        target: UCA-14
+      - type: exploits
+        target: DF-12

artifacts/stpa/ucas.yaml

@@ -1269,3 +1269,18 @@ artifacts:
         target: UCA-35
       - type: prevents
         target: H-35
+
+  - id: UCA-36
+    type: uca
+    title: Insert proof into cache APPLIED TOO LONG without max-entries bound
+    status: draft
+    description: >
+      Verification Module inserts proofs into MemoryProofCache for every verification request without enforcing a maximum entry count. An attacker submitting requests with unique module hashes causes the cache to grow without bound until memory is exhausted and the verification service is OOM-killed.
+    fields:
+      context: Cache insertion performed on every verification without an enforced maximum entry count, allowing unique-hash flood to grow MemoryProofCache unboundedly
+      uca-type: providing
+    links:
+      - type: issued-by
+        target: CTRL-4
+      - type: leads-to-hazard
+        target: H-36

scripts/vmodel/HOWTO.md

@@ -0,0 +1,123 @@
+# V-Model Gap-Hunt — Sigil
+
+A four-prompt pipeline that finds gaps in the V-model traceability graph
+(every requirement should have a test, every hazard should have a
+constraint, every approved attack-scenario should be prevented-by
+something, etc.) and produces concrete `rivet link` / `rivet add` /
+schema-edit closures.
+
+This is the V-model sibling of `scripts/mythos/`. Same Mythos discipline
+(strict oracle, fresh validator, draft emit), different domain
+(traceability completeness, not code bug-hunting).
+
+## Why this is a separate pipeline from Mythos
+
+| Axis | `scripts/mythos/` | `scripts/vmodel/` |
+|---|---|---|
+| Input | Source files (one per discovery agent) | Artifact gaps from `rivet validate` |
+| Oracle | Failing PoC test + failing Kani harness | `rivet validate` mechanical check + schema-rule satisfaction |
+| Emit | Draft `AS-N` in `artifacts/stpa/attack-scenarios.yaml` | `rivet link` command, or draft new artifact, or schema diff |
+| Question | "Is there a bug in the code?" | "Is there a gap in the trail?" |
+| Cycle | Discover → fix code → CI verifies | Discover → close gap → `rivet validate` re-runs |
+
+## Prerequisites
+
+- `rivet` installed and configured (`rivet.yaml` at repo root)
+- Permission to run `rivet validate`, `rivet link`, `rivet add`
+
+## Pipeline
+
+### 1. Rank — what to investigate first
+
+```
+Read scripts/vmodel/rank.md and execute it. Output the JSON ranking
+sorted descending. Source the gap list from `rivet validate --format json`.
+```
+
+### 2. Discover — investigate one gap per session
+
+For each tier-5 / tier-4 gap from the ranking, in a fresh session:
+
+```
+Read scripts/vmodel/discover.md and apply it to gap {{source_id}} /
+{{gap_type}}. Do not relax the oracle requirement.
+```
+
+One agent per gap is the parallelism trick. Don't sweep the whole gap
+list in a single agent — diversity of resolution proposals is the goal.
+
+### 3. Validate — fresh-session confirmation
+
+```
+Read scripts/vmodel/validate.md. Here is the proposal to validate:
+<paste discover output>
+
+Re-run rivet validate. Verify the gap still exists. Verify the
+proposal's claims by reading the artifacts and schemas it cites.
+```
+
+### 4. Emit — close the gap
+
+For confirmed proposals:
+
+```
+Read scripts/vmodel/emit.md. Here is the confirmed proposal:
+<paste validator output>
+
+Output exactly the closure artifact (rivet link command, or draft
+YAML, or schema diff). Do not narrate.
+```
+
+Then run the closure (`rivet link` directly; for new artifacts,
+human reviews the draft and decides).
+
+## Resolution categories
+
+Every confirmed gap falls into one of four:
+
+- **`link-existing`** — both artifacts exist; close with `rivet link`.
+  Highest confidence. Fully automatable.
+- **`create-and-link`** — target must be drafted first. Human reviews
+  draft, then links. Medium confidence.
+- **`schema-rule-too-strict`** — the rule shouldn't fire here. Schema
+  diff for human approval.
+- **`documented-acceptance`** — absence is intentional. Field-edit
+  citing the documentation.
+
+## Pre-release V-model check
+
+Before any release, the `rivet validate` output must show zero ERROR-level
+gaps. WARNINGs are accepted with documented justification. The pre-release
+checklist in AGENTS.md should reference this:
+
+> **V-model gap pass**: `rivet validate` passes (zero ERRORs). Any
+> WARNINGs are accepted with `risk-acceptance` field referencing
+> documentation, OR have draft closure proposals from `scripts/vmodel/`
+> queued for the next sprint.
+
+## Gotchas
+
+- **The mechanical check is the strong oracle.** `rivet validate`
+  knows whether a link exists; LLM judgment can hallucinate.
+  Always re-run rivet validate before and after any closure.
+- **Don't auto-promote draft artifacts.** `create-and-link` produces
+  draft artifacts that need human review. The reviewer is checking
+  semantic adequacy (does this test actually cover the requirement?),
+  not just structural presence.
+- **Schema-relaxation proposals need extra scrutiny.** It's tempting
+  to relax a rule when it fires "wrongly." Sometimes the rule is right
+  and the artifact graph is wrong. Default to fixing the graph, not the
+  schema.
+- **`documented-acceptance` is rare and should be questioned.** If a
+  hazard has no preventing constraint because "we accept this risk,"
+  that decision needs a real signed-off rationale, not just a comment.
+
+## Cycle
+
+```
+rivet validate (count ERRORs)
+  → rank (vmodel/rank.md)
+  → for each tier-5/4 gap: discover → validate → emit
+  → rivet validate (count ERRORs again — must decrease)
+  → repeat until ERRORs stable or zero
+```

scripts/vmodel/discover.md

@@ -0,0 +1,96 @@
+Investigate ONE traceability gap in this repository's artifact graph and
+propose a concrete resolution.
+
+Context you must use:
+- This is sigil (wsc), a security-critical cryptographic signing tool.
+  Artifacts live in `artifacts/`; schemas in `schemas/`. Rivet is the
+  traceability tool — see `AGENTS.md` for the full schema list (common,
+  dev, stpa, stpa-sec, cybersecurity).
+- Focus on ONE gap: {{source_id}} is missing {{gap_type}}.
+- The artifact graph is the audit trail. A "gap" here means an audit
+  evidence gap — auditors reading the trail cannot confirm the missing
+  property holds.
+
+Procedure (in order):
+
+1. Read the source artifact in full from `artifacts/`. Understand what
+   it claims, its status, its existing links, and any provenance fields.
+
+2. Enumerate candidates via `rivet query --sexpr` BEFORE falling back
+   to `rivet list` or YAML grep. The query DSL is the rivet-native way
+   to filter the artifact graph; use it. Examples:
+
+   - All UCAs not yet exploited by any attack-scenario:
+     `rivet query --sexpr '(and (= type "uca") (not (linked-by "exploits")))' --format ids`
+   - All requirements with no verifying test:
+     `rivet query --sexpr '(and (= type "requirement") (not (linked-by "verifies")))' --format ids`
+   - All hazards lacking a preventing constraint:
+     `rivet query --sexpr '(and (= type "hazard") (not (linked-by "prevents")))' --format ids`
+
+   Operator family: `and`, `or`, `not`, `implies`, `excludes`, `=`,
+   `!=`, `>`, `<`, `has-tag`, `has-field`, `in`, `matches`, `contains`,
+   `linked-to`, `linked-by`, `linked-from`. The semantics of the
+   `linked-*` family aren't fully self-evident — when in doubt, test
+   the predicate against a known artifact first (`rivet query --sexpr
+   '(linked-by "exploits")' --format ids` should return UCAs/data-flows
+   that ARE exploit targets).
+
+   KNOWN GAP (rivet issue #190): there is no clean predicate for
+   "this artifact is the SOURCE of an outbound link of type X." Until
+   the proposed `linked-via` operator lands, that question requires
+   `rivet validate --format json | jq` parsing. Document the fallback
+   in the COMMAND output and link issue #190.
+
+   Often the right candidate exists already; the gap is just an
+   unrecorded link.
+
+3. Check `safety/`, `docs/`, and CLAUDE/AGENTS for documented
+   scope-outs or risk acceptances that explicitly justify the absence.
+   Some gaps are intentional and documented.
+
+4. If no candidate exists AND the gap is real: identify what new
+   artifact would close it. For example:
+   - Missing `verified-by` on REQ-X → propose a new `test` artifact
+     drafting what the test would check, plus the path to where the
+     test code SHOULD live.
+   - Missing `prevented-by` on H-Y → propose a new `system-constraint`
+     that inverts the hazard.
+
+5. Distinguish four resolution categories:
+   - `link-existing` — both artifacts exist; gap is just an unrecorded
+     link. Highest-confidence resolution.
+   - `create-and-link` — the target artifact must be created (draft);
+     then linked. Medium confidence — needs human review of the draft.
+   - `schema-rule-too-strict` — the rule fires but the gap isn't
+     meaningful for this artifact type/context. Propose schema relaxation.
+   - `documented-acceptance` — the absence is intentional; the
+     artifact needs a `risk-acceptance` field or a comment citing the
+     documenting reference.
+
+Oracle requirement (non-negotiable):
+For every proposal you make you MUST produce both:
+  (1) The exact `rivet link` or `rivet add` command that would close the
+      gap (or the exact field+value to add for documented acceptance).
+      Use `--status draft` for any new artifact.
+  (2) Verification that the gap is REAL right now: paste the relevant
+      lines from `rivet validate --format json` showing the gap. After
+      your proposed action, the gap should disappear from
+      `rivet validate` output. Show this expected delta — what the next
+      `rivet validate` run would no longer report.
+
+If you cannot produce both, the proposal does not count. Do not emit
+speculative gap-closures. Hallucinations are more expensive than
+silence.
+
+Output format:
+- SOURCE: {{source_id}} (type, status, title)
+- GAP: {{gap_type}} per `rivet validate` output (paste the line)
+- INVESTIGATION: one paragraph — what you searched, what you found
+- RESOLUTION CATEGORY: link-existing | create-and-link |
+  schema-rule-too-strict | documented-acceptance
+- COMMAND: fenced shell block — the exact `rivet link` / `rivet add` /
+  field-edit
+- EXPECTED DELTA: the line that would no longer appear in
+  `rivet validate` after the action
+- CONFIDENCE: high (link-existing) | medium (create-and-link) |
+  needs-human-judgment (schema | acceptance)

scripts/vmodel/emit.md

@@ -0,0 +1,52 @@
+You are emitting the actual gap closure for a confirmed proposal. The
+emit step for V-model gaps is different from Mythos bug-emit: instead
+of drafting an artifact for human review, you are RUNNING THE COMMAND
+that closes the gap (or producing the YAML draft for a new artifact).
+
+Input:
+- Confirmed proposal (below)
+- Validator verdict: `confirmed`
+---
+{{confirmed_proposal}}
+---
+
+Rules:
+
+1. For `link-existing` resolutions:
+   - Run the exact `rivet link SOURCE -t <type> --target TARGET` command.
+   - After the command, run `rivet validate --format json` and confirm
+     the gap line disappears from the output.
+   - If the command errors (target doesn't exist, link-type invalid,
+     etc.), DO NOT retry with a different link-type. Report the error
+     and escalate to human.
+
+2. For `create-and-link` resolutions:
+   - Output the YAML draft for the new artifact, ready to paste into the
+     correct file in `artifacts/<schema>/`. Use `status: draft` always.
+   - Then output the `rivet link` command that would link the source to
+     the new artifact's ID once it's added.
+   - Do NOT execute `rivet add` directly — the new artifact requires
+     human review of the draft text before it joins the audit trail.
+
+3. For `schema-rule-too-strict` resolutions:
+   - Output the proposed change to the relevant schema file in
+     `schemas/`, as a unified diff.
+   - Do NOT apply the change; schema changes need human approval.
+
+4. For `documented-acceptance` resolutions:
+   - Output the field-edit YAML that would add the `risk-acceptance`
+     field (or whatever the schema calls the documented-exception
+     mechanism) to the source artifact.
+   - Cite the documentation reference as part of the field value.
+
+5. Closure invariant: for any resolution that lands a change, the next
+   `rivet validate --format json` MUST show one fewer gap. If it
+   doesn't, the proposal failed and must be reverted.
+
+Output exactly one of:
+- The `rivet link` command + the post-command `rivet validate` delta
+- The YAML draft + the link command + a note about human review
+- The schema diff + a note about human approval needed
+- The field-edit YAML + the documentation reference
+
+Nothing else. No prose summary, no metadata.

scripts/vmodel/rank.md

@@ -0,0 +1,53 @@
+Rank traceability gaps in this repository's artifact graph by criticality.
+Output JSON: `[{"source_id": "...", "gap_type": "...", "severity": N, "reason": "..."}]`,
+sorted by severity descending.
+
+Procedure:
+1. Run `rivet validate --format json` and parse the output.
+2. For every error, warning, and broken-cross-ref reported, classify:
+   - `gap_type`: missing-link | missing-required-field | broken-target |
+     missing-backlink | schema-violation | orphan-artifact
+   - `severity`: 1–5 per the rubric below
+   - `source_id`: the artifact id with the gap (e.g., `REQ-12`, `H-9`,
+     `UCA-6`)
+
+Severity rubric (sigil-specific, V-model criticality):
+
+5 (safety/security-critical chain — uncovered = audit-failing gap):
+  - hazard with no `prevented-by` (system-constraint missing)
+  - system-constraint with no `implements` (implementation missing)
+  - controller-constraint with no `implemented-by` (implementation
+    missing)
+  - cybersecurity-goal with no `verified-by` (cybersecurity-verification
+    missing)
+  - attack-scenario with no `prevented-by` AND status: approved
+  - uca with no `controller-constrained-by`
+
+4 (verification chain — needed for ASIL/SEC closure):
+  - cybersecurity-req with no `cybersecurity-verification` link
+  - requirement (priority `must`) with no `verified-by` (test missing)
+  - threat-scenario with no `cybersecurity-goal` (TARA outcome missing)
+  - design-decision with no `implemented-by` (ADR not actioned)
+
+3 (downstream / refinement):
+  - feature with no `requirement` link
+  - data-flow with no `security-property` (CIA gap)
+  - sub-hazard with no parent `hazard` (orphan)
+  - asset with no `threat-scenario` (TARA gap)
+
+2 (informational links):
+  - requirement (priority `should` or `nice-to-have`) with no `verified-by`
+  - traces-to links missing where helpful
+
+1 (cosmetic):
+  - missing optional fields, formatting issues
+
+When ranking:
+- A status: `approved` artifact missing a tier-5 link is an audit
+  emergency — promote one tier above its base classification.
+- A status: `draft` artifact has more latitude; promote-to-approved is
+  the natural place to backfill links, so keep its base tier.
+- If `rivet validate` reports a gap as severity ERROR, treat as ≥ tier 4
+  regardless of artifact type. WARNINGs default to tier 3.
+- Cross-reference broken targets (e.g., `links: target: H-99` where H-99
+  doesn't exist) are tier 5 — the graph is structurally broken.