fix(agent): make "verified" unearnable without verification

CHANGELOG.md

@@ -25,6 +25,18 @@ match exactly, or the workflow fails the publish.
   *Behavior change:* a drive that needs the terminal must now opt in with
   `--allow-shell`, and one that reaches a second origin must allowlist it.
 
+- **"Verified" now means verified.** A drive is finished only when the model
+  explicitly calls `finish` — a model that stops acting is an honest give-up,
+  recorded to failure-learning, never a success. A session that asserted
+  nothing is reported unverified without compiling (and the emitter refuses
+  assertion-free sessions). Emitted role/text/label locators match **exactly**
+  on both record and replay, so a later DOM addition can't silently re-target
+  a committed test. A numeric graph `schema_version` can no longer bypass the
+  compatibility guard, an empty Playwright report raises an actionable error
+  ("no tests matched — check testDir") instead of a misleading "unstable"
+  quarantine, and a target project's configured retries count each test's
+  final attempt as its outcome.
+
 ## 2026.07.1 — the "any model" release
 
 The release that makes **bring-your-own-model** mean *any* model — and proves Proofkeeper on itself. Everything since the first cut:

lore-proofkeeper/designs/design-verified-semantics.md

@@ -0,0 +1,99 @@
+---
+schema_version: 1
+id: PK-KWFVXA7HJBYQ
+type: design
+---
+# Verified Semantics — Finish, Assert, Match Exactly, Refuse Ambiguity
+
+## Context
+
+A review of the loop found the "verified" claim could be produced without
+verification: completion was inferred from a field both adapters always set,
+assertion-free sessions gated green, locators matched by substring, and two
+contract edges (numeric `schema_version`, empty or retried Playwright reports)
+were misread. This design closes each gap at its narrowest choke point.
+
+## User Need
+
+A reviewer merging a `## Verified By` link — and a maintainer reading
+`proofkeeper qa` output — must be able to trust that "verified" means: the
+model explicitly finished, at least one observable outcome was asserted, the
+committed locators mean the same thing on replay, and contract anomalies were
+refused rather than guessed at.
+
+## Design
+
+- **Finish is explicit.** `DriveResult` gains `stopReason:
+  "finished" | "gave_up" | "step_budget"` (plus `gaveUpText`); `finished` is
+  true only for an explicit `finish` tool call. The vacuous
+  `done !== undefined` check is gone. `runQa` records give-ups and budget
+  exhaustion to the learning store with distinct reasons.
+- **Assertions are required.** `sessionAssertsOutcome` (compiler IR) names the
+  assertion action types; `runQa` skips compile/gate for assertion-free
+  sessions (`QaResult.loop` becomes optional, `unverifiedReason` says why), and
+  `emitSpec` refuses them as it already refused empty sessions.
+- **Exact locators, both sides.** The emitter renders `{ exact: true }` for
+  role-name, text, and label locators, and the Recorder resolves with the same
+  exactness — record/replay agreement is the invariant, so the change is made
+  in both places in the same commit. The locator guidance tells the model to
+  copy names verbatim.
+- **Contract edges refuse, don't guess.** `parseGraph` stringifies a numeric
+  `schema_version` before comparing, so `2` is refused and `1` accepted.
+  `reduceReport` groups results per test and takes each test's final attempt
+  (retries append attempts); zero results raises `ReportParseError` naming the
+  testDir/testMatch cause instead of returning "failed".
+
+## Constraints
+
+- `QaResult.loop` optional is the only public-shape change; CLI rendering
+  guards it and prints the unverified reason.
+- Emitted specs remain byte-deterministic; the exact-matching change alters
+  emitted bytes once, uniformly.
+- No new dependency.
+
+## Rationale
+
+Each fix lands at the single point every caller flows through: the loop's stop
+handling, the emitter's refusal, the one locator-resolution seam per side, the
+one graph parser, the one report reducer. The QA loop refuses to compile
+assertion-free sessions *and* the emitter refuses them — the loop gives the
+honest verdict, the emitter makes the invariant unconditional for library
+callers.
+
+## Alternatives
+
+- **Nudge the model on a no-tool-call turn instead of stopping.** Deferred: a
+  retry prompt spends tokens to mask a model that has already disengaged;
+  honest give-up plus failure-learning steers the next attempt instead.
+- **Treat an empty report as a distinct RunStatus.** Rejected: every consumer
+  would need to handle a fourth status; an exception with a diagnostic is the
+  existing infra-failure channel.
+- **Substring locators with strict-mode suppression.** Rejected: it trades a
+  loud record-time failure for a silent wrong-element match on replay.
+
+## Accessibility
+
+Not applicable — loop semantics and parser behavior; user surface is CLI text,
+which now names why a capability is unverified.
+
+## Style Guidance
+
+Unverified reasons are complete sentences a maintainer can act on ("drive gave
+up after 4 step(s): …", "no tests matched — check testDir").
+
+## Open Questions
+
+- Whether a single retry nudge on give-up earns its token cost. Measure
+  give-up rates from the learning store first.
+
+## Related Requirements
+
+- req-verified-semantics
+
+## Related Roadmaps
+
+- autonomous-qa-enhancements
+
+## Status
+
+Accepted

lore-proofkeeper/requirements/req-verified-semantics.md

@@ -0,0 +1,63 @@
+---
+schema_version: 1
+id: PK-KWFVX9H4FDSE
+type: requirement
+---
+# "Verified" Means Verified
+
+## Problem
+
+Proofkeeper's product promise is the word "verified", and four gaps let it be
+claimed without being earned. A drive that stopped issuing tool calls was
+scored as finished (the completion check was vacuously true for both bundled
+adapters), so give-ups looked like successes and never reached the failure
+learning store. A session that asserted nothing compiled to a trivially-green
+spec and passed the fidelity gate. Emitted locators matched by substring, so a
+later DOM addition could silently re-target a committed test. And two contract
+edges misreported: a numeric graph `schema_version` bypassed the compatibility
+guard as "omitted", and a Playwright report with zero results — or with
+configured retries — was mislabelled instead of surfaced.
+
+## Requirements
+
+- [REQ-001] A drive is finished only when the model explicitly calls `finish`; a turn with no tool calls is a give-up, distinguished from the step budget, and recorded to the failure-learning store with the model's final text.
+- [REQ-002] A session with no recorded assertions is never compiled or gated: the QA loop reports it unverified with the reason, and the emitter refuses assertion-free sessions outright.
+- [REQ-003] Emitted role-name, text, and label locators match exactly, and the recorder resolves with the same exactness — an assertion that held at record time means the same thing on replay.
+- [REQ-004] A numeric graph `schema_version` counts as present: a supported value is accepted, an unsupported one is refused — it can never pass the guard as "omitted".
+- [REQ-005] A Playwright report with no test results is refused with a diagnostic naming the likely cause (spec outside the config's testDir), never silently mapped to "failed"; when the target project configures retries, each test's final attempt is its outcome.
+
+## Success Metrics
+
+- A scripted give-up drive produces `verified: false` with a give-up reason and
+  a learning record, without compiling.
+- An assertion-free session is refused by the emitter and reported unverified
+  by the QA loop.
+- A flaky-then-green retried test reduces to "passed"; an empty report raises
+  an actionable error.
+
+## Risks
+
+- Exact matching is stricter: a model that asserts a text fragment now fails at
+  record time. Mitigation: the locator guidance tells the model matching is
+  exact and to copy names verbatim; the recorder rejects at record time, so
+  nothing weaker is ever committed.
+- Give-up semantics depend on models using the `finish` tool. Mitigation: the
+  system prompt instructs it, and a non-finishing drive degrades to an honest
+  "unverified", never a false "verified".
+
+## Assumptions
+
+- The `finish` tool remains the completion signal for every adapter.
+- Playwright's JSON report continues to append one result per retry attempt,
+  final attempt last.
+
+## Related Roadmaps
+
+- autonomous-qa-enhancements
+
+## Verified By
+
+- `tests/drive-loop.test.ts`
+- `tests/compiler-emit.test.ts`
+- `tests/playwright-report.test.ts`
+- `tests/coverage.test.ts`

lore-proofkeeper/roadmaps/autonomous-qa-enhancements.md

@@ -79,6 +79,13 @@ explicit operator opt-in, navigate/request egress is allowlisted to the product
 under test, and observation side channels are redacted before reaching the model
 provider. Serves the trust outcome that underwrites every committed test.
 
+### Verified semantics
+
+Make "verified" unearnable without verification: completion only via an explicit
+finish, assertion-free sessions refused, exact locator matching on record and
+replay, and contract anomalies (schema versions, empty or retried reports)
+refused rather than guessed at. Serves the faithful-tests outcome at its core.
+
 ## Success Measures
 
 - A pull request shows exactly one Proofkeeper QA comment regardless of how many

src/agent/drive.ts

@@ -78,8 +78,16 @@ export interface DriveOptions {
 export interface DriveResult {
   /** The recorded session, ready to compile. */
   session: RecordedSession;
-  /** True if the model signalled completion (vs hitting the step budget). */
+  /** True only when the model explicitly called `finish`. */
   finished: boolean;
+  /**
+   * Why the drive ended: `finished` — the model called `finish`; `gave_up` —
+   * the model stopped issuing tool calls without finishing; `step_budget` —
+   * the turn cap was hit. Only `finished` may lead to "verified".
+   */
+  stopReason: "finished" | "gave_up" | "step_budget";
+  /** The model's final text when it gave up, for the failure-learning record. */
+  gaveUpText?: string;
   /** Number of model turns taken. */
   steps: number;
   /** The Markdown test plan, when a planning turn ran. */
@@ -297,6 +305,8 @@ export class AutonomousDriver {
 
     const maxSteps = this.options.maxSteps ?? DEFAULT_MAX_STEPS;
     let finished = false;
+    let stopReason: DriveResult["stopReason"] = "step_budget";
+    let gaveUpText: string | undefined;
     let steps = 0;
 
     while (steps < maxSteps) {
@@ -305,8 +315,11 @@ export class AutonomousDriver {
       const calls = response.toolCalls ?? [];
 
       if (calls.length === 0) {
-        // The model stopped acting; treat a `done` message as completion.
-        finished = response.done !== undefined;
+        // The model stopped issuing tool calls without calling `finish`: that is
+        // a give-up, not completion. (Adapters return text in `done` whenever
+        // there are no tool calls, so its mere presence proves nothing.)
+        stopReason = "gave_up";
+        gaveUpText = response.done?.trim() || undefined;
         break;
       }
 
@@ -318,6 +331,7 @@ export class AutonomousDriver {
         const result = await dispatch(recorder, call, policy);
         if (result.finished) {
           finished = true;
+          stopReason = "finished";
           stop = true;
           break;
         }
@@ -335,7 +349,14 @@ export class AutonomousDriver {
     monitor.dispose();
     const session = recorder.recording();
     if (plan !== undefined) session.plan = plan;
-    return { session, finished, steps, ...(plan !== undefined ? { plan } : {}) };
+    return {
+      session,
+      finished,
+      stopReason,
+      ...(gaveUpText !== undefined ? { gaveUpText } : {}),
+      steps,
+      ...(plan !== undefined ? { plan } : {}),
+    };
   }
 }
 

src/agent/tools.ts

@@ -164,6 +164,8 @@ export const LOCATOR_GUIDANCE =
   "A locator is an object { strategy: 'role'|'testId'|'text'|'label'|'css', ... }: " +
   "role needs { role, name? }, testId needs { testId }, text needs { text }, " +
   "label needs { label }, css needs { selector }. Prefer role, testId, or text over css. " +
+  "Name, text, and label matching is EXACT — copy the accessible name or visible text " +
+  "verbatim from the observation, not a fragment of it. " +
   "A locator may be passed as the `locator` field or inline on the arguments.";
 
 /** Guidance for the terminal tools, folded into the system prompt. */

src/cli.ts

@@ -517,13 +517,25 @@ async function runQaCommand(argv: string[]): Promise<number> {
 }
 
 function renderQaResult(result: Awaited<ReturnType<typeof runQa>>): string {
-  const v = result.loop.verdict;
+  const stop =
+    result.drive.stopReason === "finished"
+      ? "finished"
+      : result.drive.stopReason === "gave_up"
+        ? "gave up"
+        : "stopped at step budget";
   const lines = [
     `Capability: ${result.capability.id} — ${result.capability.title}`,
-    `Drive: ${result.drive.steps} step(s), ${result.drive.finished ? "finished" : "stopped at step budget"}`,
-    `Compiled: ${result.loop.candidate.specPath}`,
-    `Fidelity: ${v.passed}/${v.attempts} re-runs green — ${v.stable ? "stable" : "unstable, quarantined"}`,
+    `Drive: ${result.drive.steps} step(s), ${stop}`,
   ];
+  if (result.loop) {
+    const v = result.loop.verdict;
+    lines.push(
+      `Compiled: ${result.loop.candidate.specPath}`,
+      `Fidelity: ${v.passed}/${v.attempts} re-runs green — ${v.stable ? "stable" : "unstable, quarantined"}`,
+    );
+  } else {
+    lines.push(`Not compiled: ${result.unverifiedReason ?? "nothing to verify"}`);
+  }
   if (result.writeBack) {
     lines.push(
       result.writeBack.status === "proposed"

src/compiler/actions.ts

@@ -41,6 +41,25 @@ export type Action =
   | { type: "expectStatus"; status: number }
   | { type: "expectJson"; path: string; equals: string | number | boolean };
 
+/** The action types that assert an observable outcome. */
+const ASSERTION_TYPES: readonly Action["type"][] = [
+  "expectText",
+  "expectVisible",
+  "expectOutput",
+  "expectExit",
+  "expectStatus",
+  "expectJson",
+];
+
+/**
+ * Whether a session asserted at least one observable outcome. A session of
+ * bare navigation/clicks compiles to a trivially-green spec that verifies
+ * nothing — callers use this to refuse to call such a session "verified".
+ */
+export function sessionAssertsOutcome(session: RecordedSession): boolean {
+  return session.actions.some((a) => ASSERTION_TYPES.includes(a.type));
+}
+
 /** A captured drive session: its entry point and the actions recorded from it. */
 export interface RecordedSession {
   /** The capability this session exercises (threads to the write-back). */

src/compiler/emit.ts

@@ -11,7 +11,7 @@
  * (dev, prod) while still being runnable standalone.
  */
 
-import type { Action, Locator, RecordedSession } from "./actions.js";
+import { sessionAssertsOutcome, type Action, type Locator, type RecordedSession } from "./actions.js";
 
 /** Single-quoted string literal with deterministic escaping. */
 function lit(value: string): string {
@@ -24,18 +24,23 @@ function lit(value: string): string {
   return `'${escaped}'`;
 }
 
+// Name/text matching is exact: Playwright's default is substring and
+// case-insensitive, so a later DOM addition containing the same substring would
+// silently break (strict-mode violation) or mis-target a recorded locator on
+// replay. The Recorder resolves with the same exactness, so an assertion that
+// held at record time means the same thing at run time.
 function locatorExpr(loc: Locator): string {
   switch (loc.kind) {
     case "role":
       return loc.name !== undefined
-        ? `page.getByRole(${lit(loc.role)}, { name: ${lit(loc.name)} })`
+        ? `page.getByRole(${lit(loc.role)}, { name: ${lit(loc.name)}, exact: true })`
         : `page.getByRole(${lit(loc.role)})`;
     case "testId":
       return `page.getByTestId(${lit(loc.testId)})`;
     case "text":
-      return `page.getByText(${lit(loc.text)})`;
+      return `page.getByText(${lit(loc.text)}, { exact: true })`;
     case "label":
-      return `page.getByLabel(${lit(loc.label)})`;
+      return `page.getByLabel(${lit(loc.label)}, { exact: true })`;
     case "css":
       return `page.locator(${lit(loc.selector)})`;
   }
@@ -136,13 +141,20 @@ function usesHttp(session: RecordedSession): boolean {
 /**
  * Emit Playwright `.spec.ts` source for a recorded session.
  *
- * @throws {Error} when the session recorded no actions — an empty test
- *   verifies nothing and must not be emitted.
+ * @throws {Error} when the session recorded no actions, or recorded no
+ *   assertions — a test that asserts nothing verifies nothing and must not
+ *   be emitted (it would pass the fidelity gate trivially).
  */
 export function emitSpec(session: RecordedSession): string {
   if (session.actions.length === 0) {
     throw new Error("refusing to emit a test from a session with no recorded actions");
   }
+  if (!sessionAssertsOutcome(session)) {
+    throw new Error(
+      "refusing to emit a test from a session with no recorded assertions — " +
+        "a spec that asserts nothing verifies nothing",
+    );
+  }
 
   const provenance = session.capabilityId
     ? ` for capability ${session.capabilityId}`