diff --git a/docs/testing.md b/docs/testing.md
index d2ec274099..6f3b53ff5e 100644
--- a/docs/testing.md
+++ b/docs/testing.md
@@ -157,9 +157,16 @@ complete large inventories, then probes unnamed bookmarks, annotation clearing,
 batch validation before mutation, malformed addresses and regexes, segment-end
 partial reads, and synthetic file-offset rejection. Advertised schemas are
 validated in their JSON Schema dialect and successful replies are checked against
-their advertised output schemas. Disposable binary copies prove that switching
-and closing actually removes the native document, and that CLI byte results and
-invalid-address diagnostics agree with MCP. No provider is mocked in this lane.
+their advertised output schemas. Navigation checks cover interior-object cursor
+readback and mapped-memory boundaries. Annotation probes verify invalid native
+text and duplicate destinations/names before mutation, preserve unselected label
+owners, and exercise explicit batch label swaps. Function locals retain observed
+names and stack displacements. Graph probes check symbol/interior-address parity
+and a source-owned recursive cycle; literal tracing preserves complete queries
+and whitespace. Disposable binary copies prove that switching and closing
+actually removes the native document, and that CLI byte, function-dossier,
+literal-trace results and invalid-address diagnostics agree with MCP.
+No provider is mocked in this lane.
 The Linux demo lane remains a separate `verify:hopper:linux` command.
 
 Golden tests use immutable captured text inputs with producer/source provenance
diff --git a/scripts/lib/real-hopper-boundaries.mjs b/scripts/lib/real-hopper-boundaries.mjs
index 0b8279e4fc..f98d25e8ae 100644
--- a/scripts/lib/real-hopper-boundaries.mjs
+++ b/scripts/lib/real-hopper-boundaries.mjs
@@ -7,6 +7,8 @@ import { promisify } from "node:util";
 import Ajv from "ajv/dist/2020.js";
 import addFormats from "ajv-formats";
 import { mcpTextValue, requireMcpResult } from "./mcp-verifier-results.mjs";
+import { verifyHopperNavigationAndText } from "./real-hopper-navigation.mjs";
+import { verifyHopperWorkflows } from "./real-hopper-workflows.mjs";
 
 /** Exercise real Hopper annotation and malformed-input boundaries over MCP. */
 export async function verifyHopperBoundaryContracts(
@@ -47,13 +49,13 @@ export async function verifyHopperBoundaryContracts(
     successfulCalls += 1;
     return result;
   };
-  const invalid = async (name, args, reason) => {
+  const invalid = async (name, args, reason, failedOperation = name) => {
     const reply = await client.callTool({ name, arguments: args }, options);
     assert.equal(reply.isError, true, `${name} accepted invalid input`);
     const { error } = JSON.parse(mcpTextValue(reply));
     assert.equal(error.code, "invalid_request");
     assert.equal(error.category, "invalid_input");
-    assert.equal(error.details.operation, name);
+    assert.equal(error.details.operation, failedOperation);
     assert.match(error.message, reason);
     rejectedCalls += 1;
     rejectedOperations.add(name);
@@ -66,6 +68,12 @@ export async function verifyHopperBoundaryContracts(
   const foreignDocument = (await call("list_documents")).find(
     (name) => name !== activeDocument,
   );
+  const navigationAndText = await verifyHopperNavigationAndText(
+    call,
+    invalid,
+    address,
+  );
+  const workflows = await verifyHopperWorkflows(call, invalid, procedure);
   try {
     if (foreignDocument !== undefined) {
       await invalid(
@@ -268,6 +276,8 @@ export async function verifyHopperBoundaryContracts(
     rejectedCalls,
     rejectedOperations: [...rejectedOperations],
     foreignDocumentVerified: foreignDocument !== undefined,
+    navigationAndText,
+    workflows,
   };
 }
 
@@ -298,6 +308,14 @@ export async function verifyHopperLifecycleAndCli(client, options, targets) {
     await copyFile(targets.primary, primary);
     await copyFile(targets.secondary, secondary);
     await call("open_binary", { path: primary });
+    const primaryProcedures = await call("list_procedures");
+    const entry = primaryProcedures.find((item) =>
+      item.value.endsWith("rea_entry"),
+    );
+    assert.ok(entry, "primary fixture omitted its entry procedure");
+    const expectedFunction = await call("analyze_function", {
+      procedure: entry.value,
+    });
     const firstDocument = await call("current_document");
     await call("open_binary", { path: secondary });
     const secondDocument = await call("current_document");
@@ -314,6 +332,10 @@ export async function verifyHopperLifecycleAndCli(client, options, targets) {
       length: 8,
       document: secondDocument,
     });
+    await call("open_binary", { path: primary });
+    const query = "REA_C_LEAF __rea_missing_phrase__";
+    const expectedTrace = await call("trace_feature", { query });
+    assert.deepEqual(expectedTrace.matches, []);
     await call("close_binary");
 
     const dispatcher = new URL("../rea.mjs", import.meta.url).pathname;
@@ -336,6 +358,33 @@ export async function verifyHopperLifecycleAndCli(client, options, targets) {
     assert.equal(evidence.provider.id, "hopper");
     assert.equal(evidence.subject.local_path, secondary);
     assert.deepEqual(evidence.normalized_result, expected);
+    const traced = await runCli([
+      dispatcher,
+      "trace",
+      primary,
+      query,
+      "--provider",
+      "hopper",
+      "--format",
+      "json",
+    ]);
+    const traceEvidence = JSON.parse(traced.stdout);
+    assert.equal(traceEvidence.subject.local_path, primary);
+    assert.deepEqual(traceEvidence.normalized_result, expectedTrace);
+    const analyzed = await runCli([
+      dispatcher,
+      "function",
+      primary,
+      entry.value,
+      "--provider",
+      "hopper",
+      "--format",
+      "json",
+    ]);
+    assert.deepEqual(
+      JSON.parse(analyzed.stdout).normalized_result,
+      expectedFunction,
+    );
     let failure;
     try {
       await runCli([
@@ -364,6 +413,8 @@ export async function verifyHopperLifecycleAndCli(client, options, targets) {
       targetSwitchDisposedDocument: true,
       cliByteParity: true,
       cliInvalidAddress: true,
+      cliLiteralTraceParity: true,
+      cliFunctionDossierParity: true,
       callerCancellationRecovered: true,
       closedDocumentAbsent: true,
     };
diff --git a/scripts/lib/real-hopper-navigation.mjs b/scripts/lib/real-hopper-navigation.mjs
new file mode 100644
index 0000000000..9d1eb1577b
--- /dev/null
+++ b/scripts/lib/real-hopper-navigation.mjs
@@ -0,0 +1,175 @@
+import assert from "node:assert/strict";
+
+/** Verify native cursor readback and reject unrepresentable text before mutations. */
+export async function verifyHopperNavigationAndText(call, invalid, address) {
+  const cursor = await call("current_address");
+  const procedures = await call("list_procedures");
+  const other = procedures.find((item) => item.address !== address);
+  assert.ok(other, "fixture omitted a second procedure for batch validation");
+  const originalName = await call("address_name", { address });
+  const originalComment = await call("comment", { address });
+  const originalInline = await call("inline_comment", { address });
+  const originalBookmark = (await call("list_bookmarks")).find(
+    (item) => item.address === address,
+  );
+  try {
+    const instructions = await call("read_function_instructions", {
+      procedure: address,
+    });
+    const info = await call("procedure_info", { procedure: address });
+    assert.ok(info.locals.length > 0, "fixture omitted real stack locals");
+    for (const local of info.locals) {
+      assert.equal(typeof local.name, "string");
+      assert.match(local.stack_displacement, /^-?\d+$/u);
+      assert.ok(local.description.includes(local.name));
+      assert.ok(local.description.includes(local.stack_displacement));
+      assert.doesNotMatch(local.description, /object at 0x/u);
+    }
+    const dossier = await call("analyze_function", { procedure: address });
+    assert.deepEqual(dossier.procedure.locals, info.locals);
+    const coordinates = instructions.instructions.map(
+      (line) => /^0x[0-9a-f]+/u.exec(line)?.[0],
+    );
+    assert.equal(coordinates[0], address);
+    assert.ok(coordinates[1], "fixture omitted a second instruction");
+    const interior = `0x${(BigInt(address) + 1n).toString(16)}`;
+    assert.equal(await call("goto_address", { address: interior }), address);
+    assert.equal(await call("current_address"), address);
+    assert.equal(
+      await call("next_address", { address: interior }),
+      coordinates[1],
+    );
+    assert.equal(await call("prev_address", { address: interior }), address);
+    for (const unmapped of ["0x0", "0xfffffffffffffffe"]) {
+      for (const operation of ["goto_address", "next_address", "prev_address"])
+        await invalid(
+          operation,
+          { address: unmapped },
+          /Address is outside every segment/u,
+        );
+      assert.equal(await call("current_address"), address);
+    }
+    const segments = await call("list_segments");
+    const first = segments.reduce((left, right) =>
+      BigInt(left.start) < BigInt(right.start) ? left : right,
+    );
+    const last = segments.reduce((left, right) =>
+      BigInt(left.end) > BigInt(right.end) ? left : right,
+    );
+    await invalid(
+      "prev_address",
+      { address: first.start },
+      /No previous address exists in mapped memory/u,
+    );
+    await invalid(
+      "next_address",
+      { address: `0x${(BigInt(last.end) - 1n).toString(16)}` },
+      /No adjacent analyzed object exists in mapped memory/u,
+    );
+
+    const comment = "REA representation boundary 测试";
+    await call("set_comment", { address, comment });
+    await call("set_inline_comment", { address, comment });
+    await call("set_bookmark", { address, name: comment });
+    for (const [text, reason] of [
+      ["before\0after", /contains a NUL character/u],
+      ["before\ud800after", /contains an unpaired Unicode surrogate/u],
+    ]) {
+      for (const operation of ["procedure_info", "read_bytes"])
+        await invalid(
+          operation,
+          operation === "procedure_info"
+            ? { procedure: text }
+            : { address: text, length: 1 },
+          reason,
+        );
+      for (const operation of ["set_address_name", "set_bookmark"])
+        await invalid(operation, { address, name: text }, reason);
+      for (const operation of ["set_comment", "set_inline_comment"])
+        await invalid(operation, { address, comment: text }, reason);
+      await invalid(
+        "set_addresses_names",
+        { names: { [address]: "must_not_apply", [other.address]: text } },
+        reason,
+      );
+      assert.equal(await call("address_name", { address }), originalName);
+      assert.equal(
+        await call("address_name", { address: other.address }),
+        other.value,
+      );
+      assert.equal(await call("comment", { address }), comment);
+      assert.equal(await call("inline_comment", { address }), comment);
+      assert.equal(
+        (await call("list_bookmarks")).find((item) => item.address === address)
+          ?.name,
+        comment,
+      );
+    }
+    await invalid(
+      "set_address_name",
+      { address, name: other.value },
+      /already assigned to/u,
+    );
+    await invalid(
+      "set_addresses_names",
+      { names: { [address]: other.value } },
+      /already assigned to/u,
+    );
+    await invalid(
+      "set_addresses_names",
+      { names: { [address]: "duplicate", [other.address]: "duplicate" } },
+      /assigns the same name more than once/u,
+    );
+    await invalid(
+      "set_addresses_names",
+      { names: { [address]: "first", [address.slice(2)]: "second" } },
+      /selects the same address more than once/u,
+    );
+    assert.equal(await call("address_name", { address }), originalName);
+    assert.equal(
+      await call("address_name", { address: other.address }),
+      other.value,
+    );
+    try {
+      const swapped = await call("set_addresses_names", {
+        names: { [address]: other.value, [other.address]: originalName },
+      });
+      assert.equal(swapped[address], true);
+      assert.equal(swapped[other.address], true);
+      assert.equal(await call("address_name", { address }), other.value);
+      assert.equal(
+        await call("address_name", { address: other.address }),
+        originalName,
+      );
+    } finally {
+      await call("set_addresses_names", {
+        names: { [address]: originalName, [other.address]: other.value },
+      });
+    }
+    return {
+      cursorReadback: true,
+      interiorObjectNavigation: true,
+      unmappedNavigationRejected: true,
+      nativeTextValidationBeforeMutation: true,
+      unselectedLabelOwnersPreserved: true,
+      explicitLabelSwap: true,
+      observedLocalMetadata: true,
+    };
+  } finally {
+    await call("goto_address", { address: cursor });
+    await call("set_comment", { address, comment: originalComment ?? "" });
+    await call("set_inline_comment", {
+      address,
+      comment: originalInline ?? "",
+    });
+    if (originalBookmark === undefined)
+      await call("unset_bookmark", { address });
+    else
+      await call("set_bookmark", {
+        address,
+        ...(originalBookmark.name === null
+          ? {}
+          : { name: originalBookmark.name }),
+      });
+  }
+}
diff --git a/scripts/lib/real-hopper-workflows.mjs b/scripts/lib/real-hopper-workflows.mjs
new file mode 100644
index 0000000000..c0b6595edc
--- /dev/null
+++ b/scripts/lib/real-hopper-workflows.mjs
@@ -0,0 +1,86 @@
+import assert from "node:assert/strict";
+
+/** Ground literal matching and graph identity in a real provider's function chain. */
+export async function verifyHopperWorkflows(call, invalid, procedure) {
+  const address = procedure.address;
+  const originalName = await call("address_name", { address });
+  const callees = await call("procedure_callees", { procedure: address });
+  assert.ok(callees.length > 0, "fixture omitted a reachable call target");
+  const goal = callees[0];
+  const goalName = await call("address_name", { address: goal });
+  assert.equal(typeof goalName, "string");
+  const canonicalPath = await call("trace_call_path", { start: address, goal });
+  assert.equal(canonicalPath.goal_status, "reached");
+  assert.deepEqual(
+    await call("trace_call_path", { start: originalName, goal: goalName }),
+    canonicalPath,
+  );
+  assert.deepEqual(
+    await call("trace_call_path", {
+      start: address.toUpperCase(),
+      goal: `0x${(BigInt(goal) + 1n).toString(16)}`,
+    }),
+    canonicalPath,
+  );
+  const graph = await call("get_call_graph", { address });
+  assert.deepEqual(
+    await call("get_call_graph", { address: originalName }),
+    graph,
+  );
+  assert.deepEqual(
+    await call("get_call_graph", { address: address.toUpperCase() }),
+    graph,
+  );
+  const procedures = await call("list_procedures");
+  const cycle = procedures.filter((item) =>
+    /rea_cycle_[ab]$/u.test(item.value),
+  );
+  assert.equal(cycle.length, 2, "fixture omitted its source-owned call cycle");
+  const cycleGraph = await call("get_call_graph", { address: cycle[0].value });
+  const cycleNodes = Object.values(cycleGraph).flat();
+  assert.equal(cycleNodes.length, 2);
+  assert.deepEqual(
+    cycleNodes.map((node) => node.address).sort(),
+    cycle.map((item) => item.address).sort(),
+  );
+  for (const node of cycleNodes) {
+    assert.equal(node.status, "ok");
+    assert.deepEqual(
+      node.calls,
+      cycle
+        .filter((item) => item.address !== node.address)
+        .map((item) => item.address),
+    );
+  }
+  await invalid(
+    "trace_call_path",
+    { start: "__rea_missing_procedure__", goal: "__rea_missing_procedure__" },
+    /Unknown Hopper address or name/u,
+    "procedure_address",
+  );
+  const missingPhrase = await call("trace_feature", {
+    query: "REA_C_LEAF __rea_missing_phrase__",
+  });
+  assert.deepEqual(missingPhrase.matches, []);
+  assert.deepEqual(missingPhrase.references, []);
+  const phrase = "REA boundary phrase";
+  try {
+    await call("set_address_name", { address, name: phrase });
+    const traced = await call("trace_feature", { query: phrase });
+    assert.deepEqual(traced.matches, [
+      { type: "procedure", address, value: phrase },
+    ]);
+    const spaced = await call("trace_feature", { query: ` ${phrase} ` });
+    assert.deepEqual(spaced.matches, []);
+    assert.deepEqual(spaced.references, []);
+  } finally {
+    await call("set_address_name", { address, name: originalName });
+  }
+  return {
+    canonicalGraphIdentities: true,
+    sourceOwnedCallCycle: true,
+    symbolAndInteriorGoalParity: true,
+    invalidSelfPathRejected: true,
+    completeLiteralQueryPreserved: true,
+  };
+}
diff --git a/scripts/verify-real-hopper.mjs b/scripts/verify-real-hopper.mjs
index 7181c4371a..6920f2657f 100644
--- a/scripts/verify-real-hopper.mjs
+++ b/scripts/verify-real-hopper.mjs
@@ -250,7 +250,7 @@ let stderrBytes = 0;
 const stderrChunks = [];
 transport.stderr?.on("data", (chunk) => {
   stderrBytes += chunk.length;
-  if (stderrBytes <= 16_384) stderrChunks.push(chunk.toString("utf8"));
+  stderrChunks.push(chunk.toString("utf8"));
 });
 const client = new Client({ name: "real-hopper-verifier", version: "1.0.0" });
 const unrelatedHopper = await startUnrelatedHopperSentinel();
diff --git a/tests/conformance/c/fixture.c b/tests/conformance/c/fixture.c
index 38cfc2df33..07dd3a57b7 100644
--- a/tests/conformance/c/fixture.c
+++ b/tests/conformance/c/fixture.c
@@ -17,3 +17,13 @@ __attribute__((noinline, used)) int rea_entry(void) {
 }
 
 int main(void) { return rea_entry() == 12 ? 0 : 1; }
+
+__attribute__((noinline, used)) int rea_cycle_b(int value);
+
+__attribute__((noinline, used)) int rea_cycle_a(int value) {
+  return value > 0 ? rea_cycle_b(value - 1) : value;
+}
+
+__attribute__((noinline, used)) int rea_cycle_b(int value) {
+  return value > 0 ? rea_cycle_a(value - 1) : value;
+}