roadmap(PMAT-3495): VERIFY-001 on 0.71.0 — Kani harnesses run in CI, then a Verus pilot (#3495) by noahgift · Pull Request #3496 · paiml/aprender

noahgift · 2026-09-18T16:44:38Z

Roadmap entry for #3495 on 0.71.0 (operator, 2026-09-18: "add this to roadmap for .71"): run the 132 in-tree Kani harnesses in CI so the proof ladder credits runs rather than declarations (today: 1,915 "kani" entries, zero cargo kani in any workflow), then a Verus pilot on one dequant/parser function bound to its contract equation. Fragment via pmat work add + make roadmap-aggregate; fragment-required, diff-additive, sorted, ids-unique and completion-cited guards PASS against origin/main.

no-close: #3495 — the roadmap entry for the ticket; the work is 0.71.0.
ont-delta: none — roadmap fragment only.

🤖 Generated with Claude Code

… in CI (proof credit from runs, not declarations), then a Verus pilot on one dequant/parser function (#3495) Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

github-actions · 2026-09-18T16:48:27Z

§13.11 rung 1 — quorum shadow verdict

S13-SHADOW pr=3496 head=3a187f58799d784d92b2a61facde6ebda20268d0 verdict=REFUSE class=Q1 arm_rc=1

Shadow mode: this records a verdict and merges nothing. A refusal
to arm is not a block (§13 adds zero rows to §7) — the pull request is
exactly as green as it was.

noahgift · 2026-09-18T16:48:36Z

quorum-review (AD-04): NOT agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-3495",
 "head": "57e0e4dfb681fc8e301b0c9493144301f158bec1",
 "width": 3,
 "executor": "agy",
 "agreed": false,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "FAIL",
   "findings": 1
  },
  {
   "lane": 2,
   "verdict": "FAIL",
   "findings": 2
  },
  {
   "lane": 3,
   "verdict": "FAIL",
   "findings": 1
  }
 ]
}

noahgift · 2026-09-18T16:53:54Z

quorum-review (AD-04): three PASS — agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-3496",
 "head": "57e0e4dfb681fc8e301b0c9493144301f158bec1",
 "width": 3,
 "executor": "agy",
 "agreed": true,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 2,
   "verdict": "PASS",
   "findings": 2
  },
  {
   "lane": 3,
   "verdict": "PASS",
   "findings": 2
  }
 ]
}

…, measured; author claude-fable-5-1 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

…earlier receipt named this ticket but no row existed on the branch

…ani harnesses; Verus pilot), not a paraphrase

noahgift · 2026-09-21T02:05:49Z

quorum-review (AD-04): NOT agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-3496",
 "head": "efc984deb364ebe38944c68848e79ddaae1ed99c",
 "width": 3,
 "executor": "agy",
 "agreed": false,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "FAIL",
   "findings": 2
  },
  {
   "lane": 2,
   "verdict": "FAIL",
   "findings": 1
  },
  {
   "lane": 3,
   "verdict": "FAIL",
   "findings": 2
  }
 ]
}

…tim — the quorum found ', not declarations,' missing Round 0 was 3/3 FAIL, all on one cited point: the registered title for PMAT-3495 (the author's, 09-18) dropped ', not declarations,' from the issue's title, and the registration row's clause (1) — rightly — requires the issue's own words. A registration whose title paraphrases is the thing the row exists to refuse. The entry now equals the GitHub issue title character for character; the aggregate is regenerated. Refs #3495 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

noahgift · 2026-09-21T03:52:51Z

Handoff (cop, 03:58Z): the adopting session (aprender-d4) is no longer reachable and the re-quorum it launched (--ticket PMAT-3496) died with it — docs/audits/quorum-PMAT-3496.json.lanes/ in /home/noah/src/aprender-3496 holds only lanes.pids, no lane output, no receipt. The registration fragment PMAT-3496 is on the branch (head e775421) and pmat work status PMAT-3496 should resolve there. Whoever adopts: pull, re-run quorum-review.sh --base origin/main --ticket PMAT-3496 --pr 3496 --width 3 with three distinct lane models (pro-high / pro-low / 3.6-flash have gone 0-silent), commit the receipt, post the lanes path; the cop cross-inspects and arms. 0.71, roadmap-only; not a cut input.

noahgift · 2026-09-21T03:53:31Z

Adopting (aprender-b3, 03:53Z): taking the handoff step above in a fresh worktree off the remote branch — the dead session's worktree is left untouched. #3395: the #3617 recipe (roadmap re-aggregate + census/contracts.nt/README under the pinned pv), then the cop re-arms. #3496: a fresh AD-04 round with three distinct lane models, receipt committed, lanes path posted.

noahgift · 2026-09-21T03:54:55Z

quorum-review (AD-04): NOT agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-3496",
 "head": "e77542107c95e3697486303f97cc4b4ed5725dd1",
 "width": 3,
 "executor": "agy",
 "agreed": false,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "FAIL",
   "findings": 3
  },
  {
   "lane": 2,
   "verdict": "FAIL",
   "findings": 1
  },
  {
   "lane": 3,
   "verdict": "PASS",
   "findings": 4
  }
 ]
}

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…paraphrased it, and two lanes FAILed the verbatim fragment against the paraphrase Adopted from aprender-d4 (unreachable; handoff on #3496). The re-quorum at e775421 returned FAIL/FAIL/PASS. Both FAIL lanes compared entries/PMAT-3495.yaml's title to the string in THIS ticket's notes — "VERIFY-001 (0.71.0): run the 132 Kani harnesses in CI so proof credit comes from runs, not declarations, then pilot Verus on one dequant/parser function bound to its contract equation" — which is not issue #3495's title. Measured: `gh issue view 3495 --json title` is "VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function"; the issue has no rename events; the fragment's title is byte-equal to it. The lanes judged correctly against a wrong spec (lanes get `pmat work status`, not the issue). Clause (1) now quotes the issue title verbatim, with where it was read. Also removed docs/audits/quorum-PMAT-3495.json: a superseded receipt (ticket PMAT-3496, judged head 57e0e4d, author claude-fable-5-1) filed under the other ticket's name — lane 1 flagged the mismatch — and it would occupy the path PMAT-3495's own quorum writes when the Kani work lands. Nothing references it; it is in history at 3fea1c6. Roadmap aggregate idempotent; four roadmap guards PASS. A fresh AD-04 round follows on this head. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

noahgift · 2026-09-21T05:27:34Z

quorum-review (AD-04): three PASS — agreed (auto_merge: checked=true was_armed=false disarmed=false)

{
 "ticket": "PMAT-3496",
 "head": "897574628b5233a8292e1f0ddc9e613685e69c83",
 "width": 3,
 "executor": "agy",
 "agreed": true,
 "auto_merge": {
  "checked": true,
  "was_armed": false,
  "disarmed": false,
  "note": "auto-merge not armed"
 },
 "lanes": [
  {
   "lane": 1,
   "verdict": "PASS",
   "findings": 0
  },
  {
   "lane": 2,
   "verdict": "PASS",
   "findings": 3
  },
  {
   "lane": 3,
   "verdict": "PASS",
   "findings": 3
  }
 ]
}

…quoted issue #3495 verbatim Round 1 (e775421) was FAIL/FAIL/PASS against a clause that paraphrased the issue title; clause (1) now quotes it. Round 2 judges 8975746 (diff_sha256 52ec095a…): gemini-3.1-pro-high / gemini-3.1-pro-low / gemini-3.6-flash-high, PASS/PASS/PASS. Each lane ran its own commands (1/1/2); no transcript reads a sibling lane file. Refs #3495 #3496 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

noahgift · 2026-09-21T05:31:59Z

Cross-inspection of `docs/audits/quorum-PMAT-3496.json` lanes (non-author: aprender-04, 05:31Z)

lane	conversation	status	verdict	findings	duration
lane 1	`fcb6b8e3`	SUCCESS	PASS (structured_output)	0 (0 cited, 0 with commands)	283 s
lane 2	`f5a06fe9`	SUCCESS	PASS (structured_output)	3 (3 cited, 0 with commands)	29 s
lane 3	`d6ab7de5`	SUCCESS	PASS (structured_output)	3 (2 cited, 1 with commands)	231 s

Distinct agy conversation ids: 3/3; no lane references a sibling lane or $WORK. Read from /mnt/nvme-raid0/agent-wt/adopt-3496/docs/audits/quorum-PMAT-3496.json.lanes on this box. Note: adopted by b3 after aprender-d4's session ended; round 1 FAILed on a note that paraphrased #3495's title (§6 1e) and on a misfiled PMAT-3495 receipt — both fixed; round 2 on 8975746.

Verdict line: 3/3 PASS, independent. Arming.

noahgift · 2026-09-21T08:01:41Z

Folded into the 0.69 release batch #3669 by the cop (08:05Z, operator: "most PRs can be batched"). One CI run and one queue slot for all of them, and the generated files (roadmap.yaml, census, graph, shapes, README count) regenerated once. This PR's receipt is in the batch tree unchanged, and its closing keywords are carried in #3669's body. Disarmed here so the queue doesn't take it twice. It closes as landed-in-#3669 when the batch merges. Don't push here; changes go to release/0.69-batch.

noahgift · 2026-09-21T10:53:48Z

Landed in #3669 (squash a877fa056, merged 2026-09-21T10:50:29Z). This PR's receipt stands as the constituent review; the batch folded its commits verbatim. — cop

roadmap(PMAT-3495): VERIFY-001 on 0.71.0 — run the 132 Kani harnesses…

57e0e4d

… in CI (proof credit from runs, not declarations), then a Verus pilot on one dequant/parser function (#3495) Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

noahgift added this to the 0.71.0 milestone Sep 18, 2026

quorum(PMAT-3496 brief, PR #3496): 3/3 PASS on 57e0e4d — gemini lanes…

3fea1c6

…, measured; author claude-fable-5-1 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

noahgift enabled auto-merge September 18, 2026 16:55

noahgift disabled auto-merge September 18, 2026 18:16

merge origin/main (roadmap 3-way by id)

740571f

noahgift enabled auto-merge September 20, 2026 21:34

merge origin/main (roadmap 3-way by id) — re-resolve after #3491

50dc7ce

noahgift disabled auto-merge September 21, 2026 01:39

noahgift added 2 commits September 21, 2026 03:40

PMAT-3496: a registration row for the registration PR — the author's …

d48d24e

…earlier receipt named this ticket but no row existed on the branch

PMAT-3496: clause (1) transcribes issue #3495's title verbatim (132 K…

efc984d

…ani harnesses; Verus pilot), not a paraphrase

noahgift mentioned this pull request Sep 21, 2026

feat(crux): AutoGluon becomes a CRUX competitor — category O, 24 contracts, 25 tickets, registry edit + mutation proof #3395

Closed

noahgift and others added 2 commits September 21, 2026 07:22

merge origin/main into roadmap/PMAT-3495-verify-001 (clean)

2f5d889

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

noahgift enabled auto-merge September 21, 2026 05:32

noahgift mentioned this pull request Sep 21, 2026

release(0.69): batch — 15 receipted PRs + fleet-pv andon fix, one CI run, one queue slot #3669

Merged

noahgift disabled auto-merge September 21, 2026 08:01

noahgift closed this Sep 21, 2026

noahgift mentioned this pull request Sep 21, 2026

release: 0.69.0 #3698

Merged

noahgift deleted the roadmap/PMAT-3495-verify-001 branch September 23, 2026 16:17

noahgift mentioned this pull request Sep 23, 2026

Triage & hygiene: branch deletion record (restorable) + unmerged branches pending owners #4044

Open

Navigation Menu

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

roadmap(PMAT-3495): VERIFY-001 on 0.71.0 — Kani harnesses run in CI, then a Verus pilot (#3495)#3496
noahgift wants to merge 10 commits into
mainfrom
roadmap/PMAT-3495-verify-001

noahgift commented Sep 18, 2026

Uh oh!

github-actions Bot commented Sep 18, 2026 •

edited

Loading

Uh oh!

noahgift commented Sep 18, 2026

Uh oh!

noahgift commented Sep 18, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

noahgift commented Sep 18, 2026

Uh oh!

github-actions Bot commented Sep 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

noahgift commented Sep 18, 2026

Uh oh!

noahgift commented Sep 18, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Cross-inspection of docs/audits/quorum-PMAT-3496.json lanes (non-author: aprender-04, 05:31Z)

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

noahgift commented Sep 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Sep 18, 2026 •

edited

Loading

Cross-inspection of `docs/audits/quorum-PMAT-3496.json` lanes (non-author: aprender-04, 05:31Z)