diff --git a/formal/README.md b/formal/README.md
index ff3100fa..7627bced 100644
--- a/formal/README.md
+++ b/formal/README.md
@@ -16,6 +16,7 @@ the test [coordinator](./guides/GLOSSARY.md#coordinator).
 | Change a behavior or extend coverage | [AUTHORING.md](./guides/AUTHORING.md) |
 | Implement another language | [PORTING.md](./guides/PORTING.md) and [PROTOCOL.md](./guides/PROTOCOL.md) |
 | Locate or reproduce a failing check | [TEST-MAP.md](./guides/TEST-MAP.md) and the commands below |
+| See where one contract is stated, tested, challenged and mapped | `node formal/tools/where.mjs C45` (or a case, `C45.recheck-after-decode` or `B01.registration-and-policy-snapshot`) |
 | Interpret validation results | [VALIDATION.md](./guides/VALIDATION.md) |
 | Look up a term | [GLOSSARY.md](./guides/GLOSSARY.md) |
 
diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json
index b4a7585b..1b2ac7ee 100644
--- a/formal/catalogs/source-audit.json
+++ b/formal/catalogs/source-audit.json
@@ -1084,7 +1084,7 @@
   "reviewedGuides": [
     {
       "path": "formal/README.md",
-      "sha256": "bc318ab21ccd8d5589584f280ef09fdd49404596c8ce0dfedd147aa41b0f2d6e",
+      "sha256": "cb6204391896e6c69ac5ab5e6195bc1c5f07261358220bb156433b9f5599b14a",
       "entries": [
         {"title":"Executable DialCache specification"},
         {"title":"Start with your task"},
@@ -1102,7 +1102,7 @@
     },
     {
       "path": "formal/guides/AUTHORING.md",
-      "sha256": "7f3aee31a1f311f27420550960f1ceed757ecae1f1616bea01436a9635cd12f6",
+      "sha256": "728051bdcc8e1a7df19052aaa259ccdf8d7375647255325e514beafb9e22933b",
       "entries": [
         {"title":"Reading and extending the DialCache models"},
         {"title":"Reading a model"},
diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md
index c8a4221a..9f44293e 100644
--- a/formal/guides/AUTHORING.md
+++ b/formal/guides/AUTHORING.md
@@ -259,7 +259,10 @@ work in issue #165 does not need to precede unrelated feature or port developmen
 ## Give reviewers focused context
 
 For a human or LLM review, search the stable contract and case IDs first, then
-extract the matching catalog entries. Provide a small context packet:
+extract the matching catalog entries; `node formal/tools/where.mjs C45` (or a
+case ID) prints the catalog entries and model citations in one place, with
+`--json` for an agent; the validation evidence and port mappings below come
+from the reports and the replay descriptors. Provide a small context packet:
 
 - Contract/case IDs, the observable rule or change, and its documentation link.
 - Model file, exact regression/property symbols, and their execution-manifest entries.
diff --git a/formal/tools/README.md b/formal/tools/README.md
index fc8a6365..c7b90787 100644
--- a/formal/tools/README.md
+++ b/formal/tools/README.md
@@ -2,8 +2,9 @@
 
 The Node scripts behind the `make` targets. `make <target>` is
 `node formal/tools/validation.mjs <target>`; `make help` lists the targets and
-their prerequisites. Every script reads its inputs from
-[../catalogs/](../catalogs/README.md) and writes generated output only under
+their prerequisites. The scripts read their inputs from
+[../catalogs/](../catalogs/README.md) (and, for the checks and lookups over the
+text, from the models and guides) and write generated output only under
 [../generated/](../generated/README.md) and, for the witness fixtures,
 `typescript/test/fixtures/`. Start with `validation.mjs` to see
 which scripts a target runs.
@@ -12,6 +13,7 @@ which scripts a target runs.
 
 - [validation.mjs](./validation.mjs): the target dispatcher; composes every `make` target from the scripts below and checks prerequisites.
 - [execution.mjs](./execution.mjs): reads and validates the execution manifest; `node formal/tools/execution.mjs` prints the inventory.
+- [where.mjs](./where.mjs): `node formal/tools/where.mjs C45` prints where one contract, semantic case or native case is stated, tested, challenged and mapped, from the catalogs and the model comments; `--json` for agents.
 
 ## Checks
 
diff --git a/formal/tools/where.mjs b/formal/tools/where.mjs
new file mode 100644
index 00000000..4aa98d93
--- /dev/null
+++ b/formal/tools/where.mjs
@@ -0,0 +1,160 @@
+// Where a contract lives, from the catalogs the audit already parses. For one
+// contract ID (C45), one semantic case (C45.recheck-after-decode) or one native
+// case (B01.registration-and-policy-snapshot) it prints where the obligation is
+// stated (its CONTRACTS row and every model comment that cites it, ranges such
+// as "C40 to C46" included), tested (the semantic cases that carry it with
+// their scenarios, scoped Quint checks, witnesses, replays, vectors, defining
+// transitions and source pointers; the native cases that carry it with their
+// port tests; the documentation sections and tests disposed to it; the feature
+// families), challenged (the model-fault challenges that name it) and mapped
+// (the native mutants whose case carries it and the Go parity rows). No new
+// data and no gate: this is the navigation a reviewer or an agent otherwise
+// assembles by hand.
+//
+//   node formal/tools/where.mjs C45 [--json]
+import { readFileSync, readdirSync } from 'node:fs';
+import { resolve } from 'node:path';
+import { fileURLToPath } from 'node:url';
+
+export const root = fileURLToPath(new URL('../../', import.meta.url));
+const read = (path, directory) => readFileSync(resolve(directory, path), 'utf8');
+const json = (path, directory) => JSON.parse(read(path, directory));
+
+// The scheduled models and the kernel: the sources whose comments state
+// rules. The kernel fixtures exercise seams and are not scanned.
+function modelFiles(directory) {
+  const walk = relative => readdirSync(resolve(directory, relative), { withFileTypes: true }).flatMap(entry =>
+    entry.isDirectory() ? (entry.name === 'fixtures' ? [] : walk(`${relative}/${entry.name}`)) : entry.name.endsWith('.qnt') ? [`${relative}/${entry.name}`] : []);
+  return walk('formal/models').sort();
+}
+
+// Does a comment line cite the ID? A citation is the ID as a whole token, or a
+// range of the same letter that contains it: "C40-C46", "C40 to C46".
+export function cites(line, id) {
+  const letter = id[0], number = Number(id.slice(1));
+  for (const match of line.matchAll(/\b([CWEBX])(\d{2})(?:\s*(?:-|to)\s*([CWEBX])(\d{2}))?\b/g)) {
+    const [, fromLetter, from, toLetter, to] = match;
+    if (fromLetter !== letter) continue;
+    if (to === undefined) { if (Number(from) === number) return true; continue; }
+    if (toLetter === letter && Number(from) <= number && number <= Number(to)) return true;
+  }
+  return false;
+}
+
+function contractRow(id, directory) {
+  const rows = read('formal/guides/CONTRACTS.md', directory).split('\n');
+  const index = rows.findIndex(line => line.startsWith(`| ${id} |`));
+  if (index < 0) throw new Error(`${id}: not a contract in formal/guides/CONTRACTS.md`);
+  const cells = rows[index].trim().replace(/^\|\s*|\s*\|$/g, '').split(/\s*\|\s*/);
+  if (cells.length !== 3) throw new Error(`formal/guides/CONTRACTS.md:${index + 1}: expected three cells (ID, obligation, evidence), found ${cells.length}`);
+  return { line: index + 1, obligation: cells[1], evidence: cells[2] };
+}
+
+export function lookup(query, { directory = root } = {}) {
+  const match = /^([CWEBX]\d{2})(?:\.([\w-]+))?$/.exec(query ?? '');
+  if (!match) throw new Error(`${query}: expected a contract ID such as C45, a semantic case such as C45.recheck-after-decode or a native case such as B01.registration-and-policy-snapshot`);
+  const [, id, caseName] = match;
+  const caseId = caseName ? `${id}.${caseName}` : undefined;
+  const row = contractRow(id, directory);
+  const quint = modelFiles(directory).flatMap(path => read(path, directory).split('\n').flatMap((line, index) =>
+    line.trim().startsWith('//') && cites(line, id) ? [{ path, line: index + 1, text: line.trim().replace(/^\/\/\s?/, '') }] : []));
+  const coverage = json('formal/catalogs/feature-coverage.json', directory);
+  const semanticAll = json('formal/catalogs/semantic-cases.json', directory).cases.filter(entry => (entry.contracts ?? []).includes(id) || entry.id.startsWith(`${id}.`));
+  const nativeAll = (coverage.nativeCases ?? []).filter(entry => (entry.contracts ?? []).includes(id) || entry.id.startsWith(`${id}.`));
+  if (caseId && !semanticAll.some(entry => entry.id === caseId) && !nativeAll.some(entry => entry.id === caseId)) {
+    throw new Error(`${caseId}: not a semantic case in formal/catalogs/semantic-cases.json nor a native case in formal/catalogs/feature-coverage.json`);
+  }
+  const semantic = semanticAll.filter(entry => !caseId || entry.id === caseId).map(entry => ({ id: entry.id, rule: entry.rule, scenarios: entry.scenarios ?? [],
+    models: (entry.models ?? []).map(model => model.ref), definitions: (entry.definitions ?? []).map(definition => definition.ref), provenance: entry.provenance ?? [],
+    witnesses: (entry.generated ?? []).map(item => `${item.profile}/${item.witness}`), replays: entry.quintReplays ?? [], vectors: entry.vectors ?? [],
+    generatedVectors: (entry.generatedVectors ?? []).map(item => `${item.artifact}#${item.group ?? 'vectors'}/${item.name}`) }));
+  const native = nativeAll.filter(entry => !caseId || entry.id === caseId).map(entry => ({ id: entry.id, rule: entry.rule, related: entry.relatedContracts ?? [],
+    tests: ['typescript', 'go'].flatMap(port => (entry[port] ?? []).map(test => `${test.path} "${test.test}"`)), adaptation: entry.adaptation, gaps: entry.gaps ?? [], notApplicable: entry.notApplicable }));
+  const caseIds = new Set(semantic.map(entry => entry.id));
+  const audit = json('formal/catalogs/source-audit.json', directory);
+  const disposed = (audit.sources ?? []).flatMap(source => (source.entries ?? []).filter(entry => (entry.contracts ?? []).includes(id)).map(entry => ({ path: source.path, title: entry.title })));
+  const mutantsAll = json('formal/catalogs/mutations.json', directory).mutations ?? [];
+  const caseOf = new Map(mutantsAll.map(mutant => [mutant.id, mutant.case]));
+  const rust = new Map((json('formal/catalogs/rust-mutations.json', directory).mutations ?? []).map(mutant => [mutant.typescriptMutation ?? mutant.id, mutant]));
+  // Under a case query a challenge stays when its mutant sits on that case; a
+  // challenge without a port line, or one mapped across contracts, cannot be
+  // narrowed and stays with a tag saying so.
+  const challenges = (json('formal/catalogs/execution.json', directory).challenges ?? []).filter(challenge => challenge.contract === id).flatMap(challenge => {
+    const mutant = challenge.nativeMutants?.mutant, kind = challenge.nativeMutants?.kind, mutantCase = mutant ? caseOf.get(mutant) : undefined;
+    let tag;
+    if (caseId) {
+      if (!mutant) tag = `${kind}, not narrowed to a case`;
+      else if (mutantCase !== caseId) { if (!challenge.nativeMutants?.crossContract) return []; tag = `cross-contract via ${mutant} on ${mutantCase}`; }
+    } else if (challenge.nativeMutants?.crossContract) tag = `cross-contract via ${mutant} on ${mutantCase}`;
+    const profiles = challenge.reproducer?.profiles ?? [];
+    return [{ id: challenge.id, source: challenge.source, model: challenge.model, invariant: challenge.invariant, native: kind, mutant, mutantCase, tag,
+      crossContract: challenge.nativeMutants?.crossContract, run: challenge.reproducer?.run,
+      detectingProfiles: profiles.filter(profile => !profile.includes('/')).length, detectingModels: profiles.filter(profile => profile.includes('/')).length,
+      excluded: Object.keys(challenge.reproducer?.exclusions ?? {}).length }];
+  });
+  const mutants = mutantsAll.filter(mutant => caseIds.has(mutant.case)).map(mutant => ({ id: mutant.id, case: mutant.case, description: mutant.description,
+    ports: [mutant.typescript?.edits?.length ? 'typescript' : null, mutant.go?.edits?.length ? 'go' : null, rust.get(mutant.id)?.edits?.length ? 'rust' : null].filter(Boolean) }));
+  const parity = (json('formal/catalogs/go-parity.json', directory).cases ?? []).filter(entry => caseIds.has(entry.id))
+    .map(entry => ({ id: entry.id, group: entry.group, gaps: entry.gaps ?? [], nativeGo: entry.evidence?.nativeGo ?? [] }));
+  const features = (coverage.features ?? []).filter(feature => (feature.contracts ?? []).includes(id) || (feature.cases ?? []).some(entry => caseIds.has(entry)) || (feature.nativeCases ?? []).some(entry => native.some(item => item.id === entry)))
+    .map(feature => ({ id: feature.id, title: feature.title }));
+  const rule = semantic.find(entry => entry.id === caseId)?.rule ?? native.find(entry => entry.id === caseId)?.rule ?? null;
+  return { id, case: caseId ?? null, caseRule: rule, obligation: row.obligation, evidence: row.evidence, contractsLine: row.line, quint, cases: semantic, nativeCases: native, disposed, challenges, mutants, parity, features };
+}
+
+const plural = (count, word) => `${count} ${word}${count === 1 ? '' : 's'}`;
+
+export function render(result) {
+  const lines = [result.case ? `${result.case}: ${result.caseRule}` : `${result.id}: ${result.obligation}`, ''];
+  if (result.case) lines.push(`Contract ${result.id}: ${result.obligation}`, '');
+  lines.push('Stated', `  formal/guides/CONTRACTS.md:${result.contractsLine}  (evidence column: ${result.evidence})`);
+  for (const cite of result.quint) lines.push(`  ${cite.path}:${cite.line}  ${cite.text}`);
+  lines.push('', `Tested (${plural(result.cases.length, 'semantic case')}${result.nativeCases.length ? `, ${plural(result.nativeCases.length, 'native case')}` : ''})`);
+  for (const entry of result.cases) {
+    lines.push(`  ${entry.id}: ${entry.rule}`);
+    if (entry.scenarios.length) lines.push(`    scenarios: ${entry.scenarios.map(s => `"${s}"`).join(', ')}`);
+    if (entry.models.length) lines.push(`    quint checks: ${entry.models.join(', ')}`);
+    if (entry.definitions.length) lines.push(`    defining transitions: ${entry.definitions.join(', ')}`);
+    if (entry.witnesses.length) lines.push(`    witnesses: ${entry.witnesses.join(', ')}`);
+    if (entry.replays.length) lines.push(`    replays: ${entry.replays.join(', ')}`);
+    if (entry.vectors.length) lines.push(`    vectors: ${entry.vectors.join(', ')}`);
+    if (entry.generatedVectors.length) lines.push(`    generated vectors: ${entry.generatedVectors.join(', ')}`);
+    if (entry.provenance.length) lines.push(`    source: ${entry.provenance.join(', ')}`);
+  }
+  for (const entry of result.nativeCases) {
+    lines.push(`  ${entry.id}: ${entry.rule}${entry.related.length ? ` (related ${entry.related.join(', ')})` : ''}`);
+    if (entry.tests.length) lines.push(`    tests: ${entry.tests.join('; ')}`);
+    if (entry.adaptation) lines.push(`    adaptation: ${entry.adaptation}`);
+    if (entry.notApplicable) lines.push(`    not applicable: ${typeof entry.notApplicable === 'string' ? entry.notApplicable : JSON.stringify(entry.notApplicable)}`);
+    if (entry.gaps.length) lines.push(`    gaps: ${entry.gaps.map(gap => typeof gap === 'string' ? gap : JSON.stringify(gap)).join('; ')}`);
+  }
+  if (result.disposed.length) { lines.push('  disposed sections and tests (source-audit.json):'); for (const item of result.disposed) lines.push(`    ${item.path}  "${item.title}"`); }
+  if (result.features.length) lines.push(`  feature families: ${result.features.map(f => `${f.id} (${f.title})`).join('; ')}`);
+  lines.push('', `Challenged (${plural(result.challenges.length, 'challenge')})`);
+  for (const challenge of result.challenges) {
+    lines.push(`  ${challenge.id}: ${challenge.source ?? '?'} under ${challenge.model ?? '?'}:${challenge.invariant}; native ${challenge.native}${challenge.mutant ? ` ${challenge.mutant}` : ''}${challenge.run ? `; reproducer ${challenge.run}` : ''}; detected by ${plural(challenge.detectingProfiles, 'profile')}${challenge.detectingModels ? ` and ${plural(challenge.detectingModels, 'model')}` : ''}, ${challenge.excluded} excluded${challenge.tag ? ` [${challenge.tag}]` : ''}`);
+    if (challenge.crossContract) lines.push(`    cross-contract: ${challenge.crossContract}`);
+  }
+  lines.push('', `Mapped (${plural(result.mutants.length, 'native mutant')})`);
+  for (const mutant of result.mutants) lines.push(`  ${mutant.id} (${mutant.case}): ${mutant.description}; edits in ${mutant.ports.join(', ') || 'no port'}`);
+  for (const row of result.parity) lines.push(`  go-parity ${row.id}: group ${row.group}${row.gaps.length ? `; gaps ${row.gaps.length}` : ''}${row.nativeGo.length ? `; native Go ${row.nativeGo.join(', ')}` : ''}`);
+  return lines.join('\n') + '\n';
+}
+
+export function parseArguments(args) {
+  const flags = args.filter(arg => arg.startsWith('--')), positional = args.filter(arg => !arg.startsWith('--'));
+  const unknown = flags.filter(flag => flag !== '--json');
+  if (positional.length !== 1 || unknown.length) throw new Error('Usage: node formal/tools/where.mjs <contract or case, e.g. C45, C45.recheck-after-decode or B01.registration-and-policy-snapshot> [--json]');
+  return { query: positional[0], json: flags.includes('--json') };
+}
+
+if (process.argv[1] === fileURLToPath(import.meta.url)) {
+  let parsed;
+  try { parsed = parseArguments(process.argv.slice(2)); } catch (error) { console.error(error.message); process.exitCode = 2; }
+  if (parsed) {
+    try {
+      const result = lookup(parsed.query);
+      process.stdout.write(parsed.json ? `${JSON.stringify(result, null, 2)}\n` : render(result));
+    } catch (error) { console.error(error.message); process.exitCode = 1; }
+  }
+}
diff --git a/typescript/test/formal-where.test.ts b/typescript/test/formal-where.test.ts
new file mode 100644
index 00000000..e83c3bbd
--- /dev/null
+++ b/typescript/test/formal-where.test.ts
@@ -0,0 +1,92 @@
+import { describe, expect, it } from "vitest";
+
+const { lookup, render, cites, parseArguments } = await import(new URL("../../formal/tools/where.mjs", import.meta.url).href) as {
+  lookup(query: string): {
+    id: string; case: string | null; caseRule: string | null; obligation: string; contractsLine: number;
+    quint: Array<{ path: string; line: number; text: string }>;
+    cases: Array<{ id: string; scenarios: string[]; models: string[]; witnesses: string[]; provenance: string[] }>;
+    nativeCases: Array<{ id: string; tests: string[] }>;
+    disposed: Array<{ path: string; title: string }>;
+    challenges: Array<{ id: string; mutant?: string; mutantCase?: string; tag?: string; crossContract?: string; native?: string }>;
+    mutants: Array<{ id: string; case: string; ports: string[] }>; parity: Array<{ id: string }>;
+  };
+  render(result: unknown): string;
+  cites(line: string, id: string): boolean;
+  parseArguments(args: string[]): { query: string; json: boolean };
+};
+
+describe("contract lookup", () => {
+  it("finds where C45 is stated, tested, challenged and mapped from the catalogs", () => {
+    const result = lookup("C45");
+    expect(result.case).toBeNull();
+    expect(result.obligation).toMatch(/^Recheck age before\/after asynchronous decode/);
+    expect(result.quint.map(cite => cite.path)).toContain("formal/models/kernel/recovery.qnt");
+    expect(result.quint.every(cite => !cite.path.includes("/fixtures/"))).toBe(true);
+    expect(result.cases.map(entry => entry.id)).toContain("C45.recheck-after-decode");
+    expect(result.cases.every(entry => entry.scenarios.length + entry.models.length + entry.witnesses.length > 0)).toBe(true);
+    expect(result.cases.some(entry => entry.provenance.length > 0)).toBe(true);
+    expect(result.challenges.map(challenge => challenge.id)).toContain("recovery-inclusive-maximum");
+    expect(result.challenges.find(challenge => challenge.id === "recovery-future-candidate")).toMatchObject({ mutant: "M40", mutantCase: "C40.future-rejected", tag: "cross-contract via M40 on C40.future-rejected" });
+    expect(result.mutants.find(mutant => mutant.id === "M01")?.ports).toEqual(["typescript", "go", "rust"]);
+    expect(result.parity.map(row => row.id)).toEqual(result.cases.map(entry => entry.id));
+    expect(result.disposed.length).toBeGreaterThan(0);
+  });
+
+  it("selects mutants by the cases that carry the contract, so a cross-listed case keeps its mutant", () => {
+    const result = lookup("C33");
+    expect(result.cases.map(entry => entry.id)).toContain("W04.strict-fence");
+    expect(result.mutants.map(mutant => mutant.id)).toContain("M06");
+    for (const challenge of result.challenges) if (challenge.mutant && !challenge.tag) expect(result.mutants.map(mutant => mutant.id), challenge.id).toContain(challenge.mutant);
+  });
+
+  it("narrows to one semantic case and keeps unlinkable challenges with a tag", () => {
+    const narrowed = lookup("C45.maximum-age-exclusive");
+    expect(narrowed.case).toBe("C45.maximum-age-exclusive");
+    expect(narrowed.caseRule).toMatch(/exactly M preserves the source error/);
+    expect(narrowed.cases.map(entry => entry.id)).toEqual(["C45.maximum-age-exclusive"]);
+    expect(narrowed.mutants.map(mutant => mutant.id)).toEqual(["M01"]);
+    const linked = narrowed.challenges.filter(challenge => !challenge.tag);
+    expect(linked).toHaveLength(4);
+    expect(linked.every(challenge => challenge.mutant === "M01")).toBe(true);
+    expect(lookup("C45.rollback-future").challenges.map(challenge => [challenge.id, challenge.tag])).toContainEqual(["recovery-future-candidate", "cross-contract via M40 on C40.future-rejected"]);
+    const modelOnly = lookup("C24").challenges.filter(challenge => !challenge.mutant);
+    expect(modelOnly.length).toBeGreaterThan(0);
+    const firstCase = lookup("C24").cases[0]!.id;
+    expect(lookup(firstCase).challenges.filter(challenge => !challenge.mutant).map(challenge => challenge.tag)).toEqual(modelOnly.map(challenge => `${challenge.native}, not narrowed to a case`));
+  });
+
+  it("cites ranges and whole tokens, not prefixes", () => {
+    expect(cites("// Stale-on-error recovery (C40 to C46, C57)", "C42")).toBe(true);
+    expect(cites("// Selected rules from C40-C45.", "C43")).toBe(true);
+    expect(cites("// Selected rules from C40-C45.", "C46")).toBe(false);
+    expect(cites("// judged once (C43/C45)", "C45")).toBe(true);
+    expect(cites("// C450 and C4 and C455 only", "C45")).toBe(false);
+    expect(cites("// W01 to W03", "C02")).toBe(false);
+    expect(lookup("C42").quint.map(cite => cite.path)).toContain("formal/models/kernel/recovery.qnt");
+  });
+
+  it("lists native cases and their port tests for a binding contract", () => {
+    const result = lookup("B01");
+    expect(result.cases).toEqual([]);
+    expect(result.nativeCases.map(entry => entry.id)).toContain("B01.registration-and-policy-snapshot");
+    expect(result.nativeCases.every(entry => entry.tests.length > 0)).toBe(true);
+    expect(lookup("B01.registration-and-policy-snapshot").nativeCases.map(entry => entry.id)).toEqual(["B01.registration-and-policy-snapshot"]);
+  });
+
+  it("renders the four sections with clickable locations", () => {
+    const text = render(lookup("C45"));
+    for (const heading of ["Stated", "Tested (", "Challenged (", "Mapped ("]) expect(text).toContain(`\n${heading}`);
+    expect(text).toMatch(/formal\/guides\/CONTRACTS\.md:\d+/);
+    expect(text).toMatch(/formal\/models\/kernel\/recovery\.qnt:\d+/);
+    expect(text).toContain("cross-contract: ");
+    expect(render(lookup("C45.maximum-age-exclusive"))).toMatch(/^C45\.maximum-age-exclusive: After asynchronous decoding/);
+  });
+
+  it("rejects an unknown contract, a malformed query, an unknown case and bad arguments", () => {
+    expect(() => lookup("C99")).toThrow(/not a contract in formal\/guides\/CONTRACTS.md/);
+    expect(() => lookup("recovery")).toThrow(/expected a contract ID/);
+    expect(() => lookup("C45.not-a-case")).toThrow(/not a semantic case .* nor a native case/);
+    expect(parseArguments(["C45", "--json"])).toEqual({ query: "C45", json: true });
+    for (const args of [[], ["C45", "C46"], ["C45", "--jsonx"], ["--json"]]) expect(() => parseArguments(args)).toThrow(/Usage/);
+  });
+});