diff --git a/.changeset/1279-machine-proven-fail-first.md b/.changeset/1279-machine-proven-fail-first.md
index 0a06345cb..70c6662fc 100644
--- a/.changeset/1279-machine-proven-fail-first.md
+++ b/.changeset/1279-machine-proven-fail-first.md
@@ -1,10 +1,10 @@
 ---
 type: Changed
-pr: 1279
+pr: 1314
 ---
 
 **Test-tier prohibition fail-first is now MACHINE-PROVEN, not caller-attested** — the deferred literal `regression-must-fail-first` property of ADR-550 Decision 4 (the gap #1259 / PR #1273 left as a tracked follow-up) has landed. The `check prohibition-enforcement` producer (`src/prohibition-enforcement.cts`, compiled by `build:lib` to the gitignored `gsd-core/bin/lib/prohibition-enforcement.cjs`) no longer trusts the caller's `failFirst` attestation: before a clean, non-vacuous pass can dispose a `test`-tier prohibition green, the new `defaultProveFailFirst` prover independently RUNS the wired check against a KNOWN VIOLATION and confirms it goes RED. Attestation is gone from the green AND (`passed = proof.provenFailFirst === true && run.passed === true`); any other outcome — passes-on-violation, can't-prove, throws, times out, or no violation source — **hard-gates in BOTH interactive and autonomous modes** (ADR-550 D4 / D3). The evidence record gains a `failFirstProof` field recording HOW fail-first was proven (FF-07). A caller can no longer green a toothless check.
 
-The violation is sourced from a new descriptor field, **`CheckDescriptor.violationFixture`** — an author-supplied path to a known-bad subject. For a `lint-rule` the prover lints that fixture and requires the rule id to appear in the JSON report (the rule must have teeth); for a `node-test` the prover spawns the negative test with the subject injected through the **`GSD_PROHIB_SUBJECT`** env convention and requires the run to report `# fail >= 1` (the pure, mutation-pinned `isNodeTestRed` helper). The `lint-rule` path is fully shippable now and is dogfooded against the in-tree `local/no-source-grep` rule; the `node-test` path ships its mechanism (a fixture-bearing descriptor IS machine-proven) and is exercised by SYNTHETIC temp fixtures — there is no live in-tree `node --test` prohibition to dogfood. `CheckDescriptor.failFirst` is **DEMOTED, not removed** (FF-08): it is kept as a non-authoritative hint so the #1259 route-JSON shape and the `CheckDescriptor` type stay backward-compatible mid-migration, but no path greens on it alone. The green/fail-closed policy in `src/probe-core.cts` (`dispositionForProhibition`, reads only `evidence.length > 0`) is untouched; the evidence array shape is additive. This closes ADR-550's D5d follow-up — see the dated 2026-06-15 ADR-550 addendum. (#1279)
+The violation is sourced from a new descriptor field, **`CheckDescriptor.violationFixture`** — an author-supplied path to a known-bad subject. For a `lint-rule` the prover lints that fixture and requires the rule id to appear in the JSON report (the rule must have teeth); for a `node-test` the prover spawns the negative test with the subject injected through the **`GSD_PROHIB_SUBJECT`** env convention and requires a NON-VACUOUS red — `# fail >= 1` AND a failing test named distinctly from the file (`isNonVacuousNodeTestRed`), so a violation fixture that merely CRASHES the test at load is not mistaken for the negative assertion firing red (symmetric with the clean-pass non-vacuity guard). The `lint-rule` path is fully shippable now and is dogfooded against the in-tree `local/no-source-grep` rule; the `node-test` path ships its mechanism (a fixture-bearing descriptor IS machine-proven) and is exercised by SYNTHETIC temp fixtures — there is no live in-tree `node --test` prohibition to dogfood. `CheckDescriptor.failFirst` is **DEMOTED, not removed** (FF-08): it is kept as a non-authoritative hint so the #1259 route-JSON shape and the `CheckDescriptor` type stay backward-compatible mid-migration, but no path greens on it alone. The green/fail-closed policy in `src/probe-core.cts` (`dispositionForProhibition`, reads only `evidence.length > 0`) is untouched; the evidence array shape is additive. This closes ADR-550's D5d follow-up — see the dated 2026-06-15 ADR-550 addendum. (#1279)
 
-**PR-review flag — `GSD_PROHIB_SUBJECT` + `violationFixture` are PROPOSED, renamable conventions.** Both are net-new surface with ZERO live in-tree consumers (no in-tree node-test prohibition yet; node-test proof runs only on synthetic test fixtures, the real dogfood stays the lint-rule). They are forward-looking scaffolding, so a later rename — or replacing the env var with an argv — is a mechanical, zero-migration find/replace. Surfacing them here so the maintainer can **ratify, rename, or replace them at PR review** with no migration cost, exactly as #1278's ADR addendum was reviewed at PR time. The `failFirst` demotion is likewise open to weighing outright removal; the keep-as-hint rationale is recorded in the ADR addendum. (The `pr:` field above is set to the issue number #1279 because the PR is not yet open; update it to the actual PR number at open time.)
+**PR-review flag — `GSD_PROHIB_SUBJECT` + `violationFixture` are PROPOSED, renamable conventions.** Both are net-new surface with ZERO live in-tree consumers (no in-tree node-test prohibition yet; node-test proof runs only on synthetic test fixtures, the real dogfood stays the lint-rule). They are forward-looking scaffolding, so a later rename — or replacing the env var with an argv — is a mechanical, zero-migration find/replace. Surfacing them here so the maintainer can **ratify, rename, or replace them at PR review** with no migration cost, exactly as #1278's ADR addendum was reviewed at PR time. The `failFirst` demotion is likewise open to weighing outright removal; the keep-as-hint rationale is recorded in the ADR addendum.
diff --git a/docs/adr/550-spec-phase-probe-contract.md b/docs/adr/550-spec-phase-probe-contract.md
index 802439781..4a8cdd84c 100644
--- a/docs/adr/550-spec-phase-probe-contract.md
+++ b/docs/adr/550-spec-phase-probe-contract.md
@@ -99,7 +99,7 @@ This enforcement seam is the concrete instance of **ADR-857 open-question §147*
 
 ## Addendum (2026-06-15, #1279) — machine-proven fail-first REALIZED (D5d follow-up CLOSED)
 
-The 2026-06-12 addendum above closed with one honest gap to D4's literal intent: `failFirst` was **caller-ATTESTED**, not machine-proven (the note at *"Honest scope"* and the *Net effect on D4* paragraph deferred the literal `regression-must-fail-first` property to #1279). **#1279 closes that follow-up.** The literal `regression-must-fail-first` property is now **machine-proven at verify time**: before a clean pass can dispose a `test`-tier prohibition green, the producer independently RUNS the wired check against a KNOWN VIOLATION and confirms it goes RED. Any other outcome (passes-on-violation, can't-prove, throws, times out, no violation source) **hard-gates in both modes** — attestation is gone from the green AND (`passed = proof.provenFailFirst === true && run.passed === true`). The previously-deferred half of D4's intent is therefore REALIZED; the D5d follow-up is **CLOSED**. The mechanism landed in `src/prohibition-enforcement.cts` (the `defaultProveFailFirst` real prover + the pure `isNodeTestRed` helper) and is compiled by `build:lib` to the gitignored `gsd-core/bin/lib/prohibition-enforcement.cjs`.
+The 2026-06-12 addendum above closed with one honest gap to D4's literal intent: `failFirst` was **caller-ATTESTED**, not machine-proven (the note at *"Honest scope"* and the *Net effect on D4* paragraph deferred the literal `regression-must-fail-first` property to #1279). **#1279 closes that follow-up.** The literal `regression-must-fail-first` property is now **machine-proven at verify time**: before a clean pass can dispose a `test`-tier prohibition green, the producer independently RUNS the wired check against a KNOWN VIOLATION and confirms it goes RED. Any other outcome (passes-on-violation, can't-prove, throws, times out, no violation source) **hard-gates in both modes** — attestation is gone from the green AND (`passed = proof.provenFailFirst === true && run.passed === true`). The previously-deferred half of D4's intent is therefore REALIZED; the D5d follow-up is **CLOSED**. The mechanism landed in `src/prohibition-enforcement.cts` (the `defaultProveFailFirst` real prover; the node-test red proof requires a NON-VACUOUS red via `isNonVacuousNodeTestRed` — a failing test named distinctly from the file, so a load crash on the bad subject is not mistaken for the negative assertion firing red) and is compiled by `build:lib` to the gitignored `gsd-core/bin/lib/prohibition-enforcement.cjs`.
 
 This addendum ratifies three contract points: