feat(#1154): honest verifier — abstain (insufficient_spec) on non-inferable backstop truths (#1738)

* feat(verify-phase): honest verifier — abstain (insufficient_spec) on non-inferable backstop truths (#1154)

Carry the edge-probe's existing `backstop` (non-inferable) tier through the
plan-phase projection as a structured flat-scalar marker instead of a prose
parenthetical, and make verify-phase abstain -> human_needed (never silent-pass)
on a backstop truth it cannot confirm with explicit evidence. Truth-axis mirror
of #644's prohibition judgment-tier (ADR-550 D4).

Engine (deterministic, CI-tested per ADR-550 D5 — never the LLM verdict):
- src/probe-core.cts: truthStatement/truthVerification normalizers, projectTruths
  (conservative serializer), dispositionForUnverifiableTruth (backstop+no-evidence
  -> unverified/flagged/insufficient_spec; backstop+evidence -> green; inferable
  -> green, the over-abstention guard).
- src/roadmap.cts: coerceTruthToString now reads `statement` first so an object-form
  backstop truth is surfaced, not dropped (Hyrum backward-compat for truth-readers).

Workflow/agent/docs: plan-phase emits the structured marker (flat scalar, ADR-550
#1278); verify-phase + gsd-verifier add the abstain arm; new references/honest-verifier.md;
FEATURES/COMMANDS document insufficient_spec; ADR-550 amended (truth-axis D4 mirror).

Decisions adopted (trek-e review): insufficient_spec feeds existing human_needed with a
distinguishable reason (no new VERIFIER_STATUS); changeset Changed; round-trip parity
test; abstain-on-unconfirmed-backstop regression test red-first.

Implementation notes (deviations from the issue's proposed file list, verified live):
- frontmatter.cts needs no change — its flat parser already round-trips object-form truths.
- verify.cts needs no change — it grades artifacts/key_links structurally; truths are
  LLM-graded at the workflow layer, so consumption lives there + the deterministic helper.
- No CJS<->SDK hand-sync — the SDK seam was retired (ADR-0174); src/*.cts is sole source.

Regenerated artifacts: golden-install-parity fixtures, INVENTORY-MANIFEST, size baselines.

* chore(#1154): add changeset (Changed) for honest verifier

User-facing changelog fragment for #1738. Typed `Changed` (not `Added`) per
trek-e review condition 3 — the verify behavior shifts for backstop-bearing specs
(a confident silent `passed` becomes `human_needed`), which is user-visible even
though the schema marker is additive.

* docs(#1154): score-formula also excludes abstained insufficient_spec truths (review nit-1)

trek-e review nit: the verify-phase score sentence said PRESENT_BEHAVIOR_UNVERIFIED
truths were "the only ones excluded" from verified_truths. Post-#1154 an abstained
`insufficient_spec` backstop truth is also excluded (it is not ✓ VERIFIED and routes
to human_needed). Behavior was already correct; this tightens the wording.
Regenerated golden-install-parity fixtures + workflow-size baseline for the touched
verify-phase.md. (Nit-2 — a dedicated insufficient_spec_items frontmatter list — is
intentionally not taken: the current design is ADR-550-D4-conformant, the abstain
cause rides as a distinguishable report reason, and adding it would exceed the
approved scope.)

---------

Co-authored-by: Tom Boucher <trekkie@nomorestars.com>

docs/FEATURES.md

@@ -3115,7 +3115,9 @@ When a requirement's prose matches **no** shape cue, the probe does not silently
 
 The resolved edges populate a `## Edge Coverage` section in `SPEC.md`. Unresolved *applicable* edges trigger a soft gate (Resolve / Write-anyway-flagged / Keep-probing) rather than a hard block. Under `--auto`, the probe **never auto-dismisses** — it auto-covers where a defensible criterion exists, otherwise auto-backstops, and logs `[auto] edge coverage: C covered, B backstop, U unresolved`. The one exception is an `unclassified` candidate: `--auto` leaves it **`unresolved`** (surfaced as a flagged assumption), never auto-`backstop` — a missing shape is not evidence an edge exists, so minting a held-out edge obligation would be a false claim.
 
-The load-bearing wire is the `plan-phase` lift: `covered` and `backstop` edges become `must_haves.truths` the verifier can check, so the section is not merely documentation.
+The load-bearing wire is the `plan-phase` lift: `covered` and `backstop` edges become `must_haves.truths` the verifier can check, so the section is not merely documentation. A `backstop` edge is lifted as a **structured non-inferable marker** (`{ statement, verification: backstop }`, a flat scalar — not a prose note), which the **honest verifier** then consumes (see below) — closing the loop the edge-probe opened.
+
+**Honest verifier — abstention on non-inferable checks (#1154).** A non-inferable (`backstop`) truth is one whose correct behavior is not derivable from the spec alone, so the verifier cannot self-detect the gap and would confidently false-pass it (~100% of the time). At verify time, a `backstop` truth the verifier cannot confirm with **explicit evidence** (a passing wired held-out/property-based test, or a directly-observed behavior) **abstains** → `human_needed` with reason `insufficient_spec` (reported as `unverified — held-out test recommended`), **never a silent `passed`**. This is the verify-time, truth-axis mirror of the prohibition judgment-tier disposition (ADR-550 D4): exogenous (driven by the `backstop` tag, never a self-judged "abstain if unsure"), routing-not-diagnosis (the held-out test carries the omitted rule), and capable-tier dependent (reliable on `sonnet`+; the budget `haiku` tier degrades toward current behavior). An inferable truth is never abstained (the over-abstention guard). Reference: [Honest Verifier](../gsd-core/references/honest-verifier.md).
 
 **Requirements:**
 - REQ-EDGE-01: The edge pass MUST run after the ambiguity gate and emit a `## Edge Coverage` SPEC section.
@@ -3125,6 +3127,8 @@ The load-bearing wire is the `plan-phase` lift: `covered` and `backstop` edges b
 - REQ-EDGE-05: `--auto` MUST never auto-dismiss — auto-cover or auto-backstop only.
 - REQ-EDGE-06: `plan-phase` MUST lift `covered` criteria and `backstop` notes into `must_haves.truths`.
 - REQ-EDGE-07: A requirement whose prose matches no shape cue MUST surface an `unclassified — review manually` candidate (never silently dropped); `--auto` MUST leave it `unresolved`, never auto-`backstop`.
+- REQ-EDGE-08: `plan-phase` MUST lift a `backstop` edge into `must_haves.truths` as a structured flat-scalar marker (`{ statement, verification: backstop }`), never a prose parenthetical.
+- REQ-HONEST-01: At verify time a `backstop` truth that cannot be confirmed with explicit evidence MUST abstain → `human_needed` (reason `insufficient_spec`), never `passed`; an inferable truth MUST never be abstained (over-abstention guard); abstention MUST be exogenous (driven by the `backstop` tag, not self-judgment).
 
 **Reference:** [Edge Probe](../gsd-core/references/edge-probe.md)