roadmap(PMAT-3495): VERIFY-001 on 0.71.0 — Kani harnesses run in CI, then a Verus pilot (#3495)

docs/audits/quorum-PMAT-3496.json

@@ -0,0 +1,180 @@
+{
+  "ticket": "PMAT-3496",
+  "base": "origin/main",
+  "base_resolved": "origin/main",
+  "base_note": "no origin/origin/main exists; judged against the local ref",
+  "head": "897574628b5233a8292e1f0ddc9e613685e69c83",
+  "diff_sha256": "52ec095a43bb1195ade36a752d71b633f8a5f90d1f39329477ef90ea93e4acfe",
+  "width": 3,
+  "executor": "agy",
+  "prompt_mode": "inline",
+  "prompt_bytes": 5239,
+  "author": {
+    "model": "claude-opus-5",
+    "family": "claude",
+    "source": "flag"
+  },
+  "agreed": true,
+  "lanes": [
+    {
+      "lane": 1,
+      "status": "SUCCESS",
+      "verdict": "PASS",
+      "summary": "The diff perfectly implements the acceptance criteria for PMAT-3496. It creates `docs/roadmaps/entries/PMAT-3495.yaml` and `docs/roadmaps/entries/PMAT-3496.yaml` with the precise titles specified in the ticket. It also adds these entries to `docs/roadmaps/roadmap.yaml`. The diff is strictly additive and touches nothing outside of `docs/roadmaps/`, with no unauthorized changes (e.g. no Kani harnesses or CI wiring included). No flaws or regressions were found.",
+      "findings": [],
+      "raw_bytes": 3186,
+      "err_bytes": 100,
+      "envelope_status": "SUCCESS",
+      "verdict_source": "structured_output",
+      "grounding_check": "parity",
+      "model": "gemini-3.1-pro-high",
+      "model_measured": "gemini-3.1-pro-high",
+      "model_source": "measured",
+      "family": "gemini"
+    },
+    {
+      "lane": 2,
+      "status": "SUCCESS",
+      "verdict": "PASS",
+      "summary": "The diff correctly implements PMAT-3496 by registering PMAT-3495 and PMAT-3496 in the roadmap. The titles are transcribed verbatim, and the diff only touches the permitted roadmap files.",
+      "findings": [
+        {
+          "claim": "The title for PMAT-3495 is transcribed verbatim as required by the acceptance criteria of PMAT-3496.",
+          "file": "docs/roadmaps/entries/PMAT-3495.yaml",
+          "grounding": "cited",
+          "line": 4
+        },
+        {
+          "claim": "The title for PMAT-3496 matches the ticket's title exactly.",
+          "file": "docs/roadmaps/entries/PMAT-3496.yaml",
+          "grounding": "cited",
+          "line": 4
+        },
+        {
+          "claim": "The roadmap.yaml file is additively updated with the new entries, matching the individual files.",
+          "file": "docs/roadmaps/roadmap.yaml",
+          "grounding": "cited",
+          "line": 18631
+        }
+      ],
+      "raw_bytes": 3577,
+      "err_bytes": 0,
+      "envelope_status": "SUCCESS",
+      "verdict_source": "structured_output",
+      "grounding_check": "parity",
+      "model": "gemini-3.1-pro-low",
+      "model_measured": "gemini-3.1-pro-low",
+      "model_source": "measured",
+      "family": "gemini"
+    },
+    {
+      "lane": 3,
+      "status": "SUCCESS",
+      "verdict": "PASS",
+      "summary": "Lane 3 Reviewer verdict: PASS. The diff registers PMAT-3495 and PMAT-3496 in the roadmap entries directory and additively updates docs/roadmaps/roadmap.yaml. All acceptance criteria are satisfied: PMAT-3495 title matches issue #3495 verbatim, the roadmap YAML changes are purely additive (0 deletions, 0 reserialisations), valid YAML syntax is maintained, and no files outside docs/roadmaps/ are touched.",
+      "findings": [
+        {
+          "claim": "docs/roadmaps/entries/PMAT-3495.yaml creates entry PMAT-3495 with issue 3495 and exact title matching issue #3495 verbatim",
+          "file": "docs/roadmaps/entries/PMAT-3495.yaml",
+          "fix": "N/A",
+          "grounding": "cited",
+          "line": 1
+        },
+        {
+          "claim": "docs/roadmaps/entries/PMAT-3496.yaml creates entry PMAT-3496 with issue 3495 and exact title matching ticket PMAT-3496 verbatim",
+          "file": "docs/roadmaps/entries/PMAT-3496.yaml",
+          "fix": "N/A",
+          "grounding": "cited",
+          "line": 1
+        },
+        {
+          "claim": "docs/roadmaps/roadmap.yaml additively aggregates entries PMAT-3495 and PMAT-3496 with 0 deletions or reserialisations and valid YAML syntax",
+          "command": "python3 -c \"import yaml; diff_pmat3495 = '''- id: PMAT-3495\\n  github_issue: 3495\\n  item_type: task\\n  title: 'VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function'\\n  status: planned\\n  priority: medium\\n  assigned_to: null\\n  created: 2026-09-18T16:43:48Z\\n  updated: 2026-09-18T16:43:48Z\\n  spec: null\\n  acceptance_criteria: []\\n  phases: []\\n  subtasks: []\\n  estimated_effort: null\\n  labels: []\\n  notes: null'''; diff_pmat3496 = '''- id: PMAT-3496\\n  github_issue: 3495\\n  item_type: task\\n  title: 'Register PMAT-3495 (VERIFY-001 on 0.71.0) in the roadmap so the AD-04 quorum for PR #3496 can run (registration only)'\\n  status: planned\\n  priority: medium\\n  assigned_to: null\\n  created: 2026-09-21T01:39:59Z\\n  updated: 2026-09-21T01:39:59Z\\n  spec: null\\n  acceptance_criteria: []\\n  phases: []\\n  subtasks: []\\n  estimated_effort: null\\n  labels:\\n  - kind:triage\\n  notes: \\\"ACCEPTANCE...\\\"'''; parsed_3495 = yaml.safe_load(diff_pmat3495); parsed_3496 = yaml.safe_load(diff_pmat3496); assert parsed_3495[0]['id'] == 'PMAT-3495'; assert parsed_3496[0]['id'] == 'PMAT-3496'; print('YAML validation passed cleanly!')\"",
+          "file": "docs/roadmaps/roadmap.yaml",
+          "fix": "N/A",
+          "grounding": "measured",
+          "line": 18631,
+          "output": "no git remotes found\nYAML validation passed cleanly!"
+        }
+      ],
+      "raw_bytes": 7249,
+      "err_bytes": 0,
+      "envelope_status": "SUCCESS",
+      "verdict_source": "structured_output",
+      "grounding_check": "parity",
+      "model": "gemini-3.6-flash-high",
+      "model_measured": "gemini-3.6-flash-high",
+      "model_source": "measured",
+      "family": "gemini"
+    }
+  ],
+  "dissent": [],
+  "dedup": [
+    {
+      "file": "docs/roadmaps/entries/PMAT-3495.yaml",
+      "line": 1,
+      "lanes_agreeing": [
+        3
+      ],
+      "claims": [
+        "docs/roadmaps/entries/PMAT-3495.yaml creates entry PMAT-3495 with issue 3495 and exact title matching issue #3495 verbatim"
+      ]
+    },
+    {
+      "file": "docs/roadmaps/entries/PMAT-3495.yaml",
+      "line": 4,
+      "lanes_agreeing": [
+        2
+      ],
+      "claims": [
+        "The title for PMAT-3495 is transcribed verbatim as required by the acceptance criteria of PMAT-3496."
+      ]
+    },
+    {
+      "file": "docs/roadmaps/entries/PMAT-3496.yaml",
+      "line": 1,
+      "lanes_agreeing": [
+        3
+      ],
+      "claims": [
+        "docs/roadmaps/entries/PMAT-3496.yaml creates entry PMAT-3496 with issue 3495 and exact title matching ticket PMAT-3496 verbatim"
+      ]
+    },
+    {
+      "file": "docs/roadmaps/entries/PMAT-3496.yaml",
+      "line": 4,
+      "lanes_agreeing": [
+        2
+      ],
+      "claims": [
+        "The title for PMAT-3496 matches the ticket's title exactly."
+      ]
+    },
+    {
+      "file": "docs/roadmaps/roadmap.yaml",
+      "line": 18631,
+      "lanes_agreeing": [
+        2,
+        3
+      ],
+      "claims": [
+        "The roadmap.yaml file is additively updated with the new entries, matching the individual files.",
+        "docs/roadmaps/roadmap.yaml additively aggregates entries PMAT-3495 and PMAT-3496 with 0 deletions or reserialisations and valid YAML syntax"
+      ]
+    }
+  ],
+  "uncovered": [],
+  "coverage_source": "lanes",
+  "partial": false,
+  "partial_reasons": [],
+  "auto_merge": {
+    "checked": true,
+    "was_armed": false,
+    "disarmed": false,
+    "note": "auto-merge not armed"
+  },
+  "lint": {
+    "ok": true,
+    "output": "receipt complete: kind=artifact lanes=3 author=claude-opus-5/claude"
+  }
+}

docs/roadmaps/entries/PMAT-3495.yaml

@@ -0,0 +1,16 @@
+- id: PMAT-3495
+  github_issue: 3495
+  item_type: task
+  title: 'VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function'
+  status: planned
+  priority: medium
+  assigned_to: null
+  created: 2026-09-18T16:43:48Z
+  updated: 2026-09-18T16:43:48Z
+  spec: null
+  acceptance_criteria: []
+  phases: []
+  subtasks: []
+  estimated_effort: null
+  labels: []
+  notes: null

docs/roadmaps/entries/PMAT-3496.yaml

@@ -0,0 +1,17 @@
+- id: PMAT-3496
+  github_issue: 3495
+  item_type: task
+  title: 'Register PMAT-3495 (VERIFY-001 on 0.71.0) in the roadmap so the AD-04 quorum for PR #3496 can run (registration only)'
+  status: planned
+  priority: medium
+  assigned_to: null
+  created: 2026-09-21T01:39:59Z
+  updated: 2026-09-21T01:39:59Z
+  spec: null
+  acceptance_criteria: []
+  phases: []
+  subtasks: []
+  estimated_effort: null
+  labels:
+  - kind:triage
+  notes: 'ACCEPTANCE (this row is PR #3496 itself, a roadmap-only registration): (1) docs/roadmaps/entries/PMAT-3495.yaml exists with id PMAT-3495, github_issue 3495, and a title that transcribes issue #3495''s title VERBATIM, character for character: "VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function" (read from `gh issue view 3495 --json title` on 2026-09-21; the issue has no rename events); (2) docs/roadmaps/roadmap.yaml equals aggregate(entries/) and the diff vs origin/main is additive only (deleted=0, reserialised=0) after the merges of origin/main; (3) the PR touches nothing outside docs/roadmaps/ and docs/audits/. NOT in scope: any Kani harness, CI wiring or proof — those are PMAT-3495''s own work and are judged when it lands. A lane that finds the entry mis-transcribed, missing or invented FAILs this row.'

docs/roadmaps/roadmap.yaml

@@ -18628,6 +18628,39 @@ roadmap:
   estimated_effort: null
   labels: []
   notes: null
+- id: PMAT-3495
+  github_issue: 3495
+  item_type: task
+  title: 'VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function'
+  status: planned
+  priority: medium
+  assigned_to: null
+  created: 2026-09-18T16:43:48Z
+  updated: 2026-09-18T16:43:48Z
+  spec: null
+  acceptance_criteria: []
+  phases: []
+  subtasks: []
+  estimated_effort: null
+  labels: []
+  notes: null
+- id: PMAT-3496
+  github_issue: 3495
+  item_type: task
+  title: 'Register PMAT-3495 (VERIFY-001 on 0.71.0) in the roadmap so the AD-04 quorum for PR #3496 can run (registration only)'
+  status: planned
+  priority: medium
+  assigned_to: null
+  created: 2026-09-21T01:39:59Z
+  updated: 2026-09-21T01:39:59Z
+  spec: null
+  acceptance_criteria: []
+  phases: []
+  subtasks: []
+  estimated_effort: null
+  labels:
+  - kind:triage
+  notes: 'ACCEPTANCE (this row is PR #3496 itself, a roadmap-only registration): (1) docs/roadmaps/entries/PMAT-3495.yaml exists with id PMAT-3495, github_issue 3495, and a title that transcribes issue #3495''s title VERBATIM, character for character: "VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function" (read from `gh issue view 3495 --json title` on 2026-09-21; the issue has no rename events); (2) docs/roadmaps/roadmap.yaml equals aggregate(entries/) and the diff vs origin/main is additive only (deleted=0, reserialised=0) after the merges of origin/main; (3) the PR touches nothing outside docs/roadmaps/ and docs/audits/. NOT in scope: any Kani harness, CI wiring or proof — those are PMAT-3495''s own work and are judged when it lands. A lane that finds the entry mis-transcribed, missing or invented FAILs this row.'
 - id: PMAT-3500
   github_issue: 3500
   item_type: task