Verification

How the workspace answers "is this right?" — the LaTeX compiler, the Lean 4 checker, the Claim Verifier, the faithfulness audit — through ONE contract, so every verifier is added the same way, shows up in the same places, and never claims more than it checked. It is rendered publicly at /docs/verification and is the single source of truth for this vocabulary (tests/ui/verification-doc.test.ts fails when the registry and this page drift). The shell it plugs into is the Workspace SDK.

One word per concept:

Term	Means	In code
Verifier	Something that checks a piece of the document and returns verdicts.	VerifierSpec, lib/workspace/verifiers.ts
Subject	What one verdict is about: the whole document, one statement, one claim, or one link between artifacts.	VerifierSubject
Verdict	The verifier's own word for a result (proved, sorry, contradicted, faithful, …).	VerifierSpec.verdicts
Status	The shared five-value vocabulary every surface renders.	VerifierStatus: ok, conditional, warn, error, pending
Surface	Where a status shows: header chip, gutter glyph, glyph card, companion leaf, tie anchor.	§3
Evidence	The real output behind a verdict, always one click from the status.	VerifierSpec.evidence

Sections: the contract (§1), the built-ins (§2), where a status shows (§3), the Modules rail (§4), colors (§5), how to add one (§6), tests (§7), what each built-in is made of (§8, with the formalization campaign in §8.1), the code map (§9), open seams (§10), the manifest (§11).

1. The contract

A verifier is declared once, with registerVerifier:

registerVerifier({
  id: 'lean',                 // also the glyph kind: sd-glyph-lean
  label: 'Lean 4',
  subject: 'statement',       // document | statement | claim | link
  trigger: 'auto',            // auto (every settled edit) | manual (a button) | agent (a run)
  verdicts: ['proved', 'conditional', 'sorry', 'error', 'pending'],
  status: (v) => ({ proved: 'ok', conditional: 'conditional', sorry: 'warn', error: 'error' }[v] ?? 'pending'),
  glyph: true,                // draws in the editor's status lane
  companion: 'lean',          // the leaf that shows its full output
  evidence: "the compiler's real output on the Lean chip, and the declaration in the Lean leaf",
  module: 'lean-blueprint',   // the catalog module that installs it; null = built in
  pitch: 'Checks each theorem against a Lean 4 proof.', // the rail's Recommended row
  recommend: (paths) => paths.some((p) => /\.tex$/i.test(p)), // which files call for it
  documents: ['.tex', '.lean'], // files it applies to once on; empty = every text document
  resultInstruction: '…',     // for an agent-written verdict: the output contract every reader parses
});

Which verifiers a workspace has ON is the installed modules' call: a module's manifest declares verifies: [lean, audit], the page reads its installed modules (useWorkspaceVerifiers → GET /api/workspace/modules), and activeVerifiers({ path, enabled }) answers "which verifiers apply to this file right now". There is no slug list and no file sniff; the compiler is built in (module: null) and needs no module.

Four rules make the contract hold:

1. Enablement is declared, never inferred. A module says verifies: [id]; the workspace is on for those ids while the module is installed. Adding a Lean module from the sidebar lights the same surfaces as creating the workspace from it; removing it darkens them.
2. Verdicts stay the verifier's own words. proved, sorry, contradicted, faithful — never pre-translated. The mapping to the shared status lives in the spec (status) and nowhere else; verifierStatus(id, verdict) is the only way a surface asks. Words are compared trimmed and lowercased (normalizeVerdict), so a checker that prints Proved still lands; a word the spec never declared, an unknown verifier, or an empty verdict is pending — never a guess.
3. There are five statuses, and a verifier never invents a sixth. ok right · conditional right modulo something still open (proved modulo an open lemma, faithful in part) · warn not wrong, not done (a sorry, a hedged report, a stale compile) · error wrong (a compile error, a contradicted claim, a mismatch) · pending not checked yet.
4. Every status links to its evidence. The chip opens the log, the glyph card shows the other side and the report, the leaf shows the real output. A status without evidence is not shown.

registerVerifier refuses a spec the surfaces could not render honestly — a malformed id (lowercase letters, digits, dashes), no verdict words, a verdict that is not lowercase and trimmed, or one whose mapping lands outside the five statuses — by throwing at registration, not by showing a blank glyph later. Registering an id again replaces the earlier spec; the returned unregister function only removes the spec it registered.

2. The built-in verifiers

id	Checks	Trigger	Verdicts → status	Shows in
compile	the document — LaTeX compiles on the Modal pool	auto (every settled edit with auto-compile on; Recompile otherwise)	compiled ok · warning warn · error error · stale warn · compiling pending	header chip (Recompile + status), gutter glyph per diagnostic line, the PDF leaf
lean	one statement — its Lean declaration on the prover pool	auto (the sibling .lean is re-checked as it changes, debounced, and while a formalization run is live)	proved ok · conditional conditional · sorry warn · error error · assumed ok · pending pending	header chip (Lean n/m), L4 gutter glyph on the statement and on the declaration, the Lean leaf, the graph node
claim	one claim — a sentence, by the Claim Verifier assistant	agent (Verify n runs every statement; a selection runs one)	not_contradicted ok · unsettled warn · contradicted error · failed warn · pending pending	quote gutter glyph on the claim, its card, the verification thread and its chat
audit	one link — does the declaration say what the statement says?	agent (the faithfulness audit run writes <stem>.audit.json)	faithful ok · partial warn · mismatch error · unstated error · refuted error	the graph node's ring, the Graph leaf's progress chip

What a status must never say: not_contradicted is not "true" — only that the checked evidence found no direct conflict; a report that says "not contradicted" but admits thin evidence is unsettled (the card says so), never a quiet green. conditional is not ok — it is proved modulo open lemmas, drawn as a hollow ring so the difference is visible from the gutter. unstated is an error, not a warning: a declaration with no statement behind it is a claim the paper never made. stale is a warning on a PDF that no longer matches the source.

Edge cases the surfaces handle the same way for every verifier:

• Two verdicts on one line (a theorem that is a Lean statement and a verified claim): the worst status wins, then the higher glyphRank (Lean 3, compile 2, claim 1); the rest ride along on the card.
• No verdict yet (a run in flight, a check that never answered): pending — a hollow or faded glyph, a "Checking" chip — never an inferred ok.
• A verdict for a line that moved (the file was edited after the run): glyphs anchor to line ranges the editor keeps in step with edits; a verdict the editor can no longer place is dropped, not drawn on the wrong line.
• A verifier whose module is not installed (activeVerifiers leaves it out): its chip and glyphs are absent, not pending.

3. Surfaces

Every verifier lands on the same surfaces; a verifier opts into each by what it declares (glyph, companion, subject).

• Header chip — the file's own header row carries the cluster: Recompile with the compile status, Lean n/m (the Formalize button before a sibling exists), Verify n, then the PDF | Lean | Graph companion switch. The chip is the one place a document-level status lives; clicking it opens the evidence (log, statement list, run chat).
• Gutter glyph — one glyph per line in the editor's status lane, left of the line numbers, centered between the pane edge and the number. Kind is the shape (L4 chip, page, quote mark), status is the color (green, hollow green, orange, red, hollow). On a line with several, the worst status wins and Lean ranks over compile over claim; the rest ride along on the card (mergeGutterGlyphs).
• Glyph card — hover a glyph: the verdict in words, the other side's excerpt (the declaration for a statement, the log rows for a compile, the report for a claim), Logs / PDF / Lean / Graph / Tie all.
• Companion leaf — the verifier's full output as a view beside the source (pdf, lean, graph in the view registry), an ordinary pane with the shared header, never a side panel.
• Tie anchor — a verdict's subject is a tie member: double-click the statement and the connectors run to its declaration, its graph node, its PDF line, the chat that wrote it and the thread that checked it.
• Agent hand-off — a failing verdict offers the fix: "Fix with agent" on a compile error, "Fix it with the agent" on a sorry, the chat behind a contradicted claim. The verifier reports; the agent repairs; the verifier re-runs.

4. Modules: adding and removing a verifier

Verifiers are modules, and Modules is the first section of the rail — what is switched on reads before the files it checks. The section lists:

• Installed verifiers first, one row each: a status dot in the shared palette (the worst status in the open document), the verifier's name, and its own summary in its own words — compiled, 1/1 proved, 2 checked, none contradicted, 3 audited, 1 flagged. Clicking a row opens its evidence: the PDF, Lean or Graph leaf, or the verifying chat. The compiler is built in: it has a row and no Remove.
• Other installed modules by name.
• Recommended: the verifiers this workspace's files would use but has not added (recommendedVerifiers(paths, installed): a .tex recommends Lean 4 and the Claim Verifier, a .lean the audit), each with its pitch and one Add. Two verifiers can share a module — Lean and the audit both come with lean-blueprint — so Recommended shows one row per module.
• Browse the gallery, where verifiers lead as "Checks your work" and carry the Verifier kind.

Add runs the connect route for VerifierSpec.module: files seed at the root, instructions append, the row moves up with a pending dot, and the header cluster gains its chip. The first verdict turns the dot. Remove asks first and says what goes: the status chip and the gutter glyphs disappear; threads, chats and the files it added stay. Readers see the rows and statuses with no Add or Remove.

What a row must never do: report another document's status (the summary is for the open document, and says open a .tex to check when none is), or show a verifier as pending when it simply does not apply here (no .tex in this workspace).

5. Status colors

status	color	glyph
ok	green	filled
conditional	green	hollow ring
warn	orange	filled
error	red	filled
pending	stone	hollow (L4), faded (page, quote)

app/globals.css .sd-glyph-<status> sets the color; .sd-glyph-<kind> the shape. STATUS_COLOR in verifiers.ts is the same palette for SVG surfaces (the graph's node dots and audit affixes), so a status is one color everywhere.

6. Adding a verifier

1. registerVerifier its spec in lib/workspace/verifiers.ts: id, subject, trigger, its own verdict words, the status mapping, whether it glyphs, which companion shows its output, where its evidence lives, the catalog module that installs it (module, null for a built-in), its one-line pitch, recommend — which workspace files call for it — and which files it applies to once on (documents).
2. Have the module that ships it declare verifies: [id] in its manifest (§11). An action that produces its verdict names it (verifier: id) and says where the answer lands (result: thread for an annotation on the selection, else a chat); enabled_by_default and model are the action's other knobs. The invoke route reads those — never an identity.
3. Produce verdicts with a subject anchor: a line range in the file ({ line, endLine }) for a document or statement verdict, a thread for a claim, a declaration name for a link. Anchors are what the glyph lane, the graph and the ties consume.
4. If it glyphs, feed GutterGlyphs into the merge (kind = its id) with a glyphRank in the spec — GlyphKind is any registered id, so the lane, the card, the merge order and the colors need no edits. Add the glyph shape in globals.css (.sd-glyph-<id>::before).
5. If it has a chip, add a renderer to the page's verifierChips table (a VerifierChip); the header cluster (LatexCompileControls) renders the chips of the active verifiers in registry order and knows none by name.
6. If it needs a full view, register a companion leaf in the view registry (registerView, TexCompanionMode) — see the Workspace SDK §12.
7. If a failing verdict has a repair, offer the agent hand-off from the evidence, never from the status alone.
8. Give the rail its status and summary: verifierRows in page.tsx maps the verifier's id to { status, summary, onOpen } from its pipeline.
9. Add its row to §2 above and a test in tests/ui/verifiers.test.ts; the doc test fails until the row exists.

7. Tests

Verifier	Unit	API	Smoke
compile	tests/ui/use-latex-compile-*.test.ts, use-latex-autofix.test.tsx, latex-editor-toolbar.test.tsx, latex-pdf-viewer.test.tsx, tests/latex/*, tests/lib/latex-*.test.ts, agent-ts/tests/latex-autofix.test.ts	tests/api/workspace-compile-route.test.ts	tests/smoke/workspace-latex.spec.ts (@latex)
lean, audit	tests/lib/formalization-*.test.ts, tests/ui/latex-formalize-cluster.test.tsx, lean-status-chip.test.tsx, lean-statement-links.test.tsx, tests/lib/gutter-glyphs.test.ts, agent-ts/tests/search-lean-tool.test.ts	tests/api/lean-check-route.test.ts, assistants-connect-route.test.ts	none yet
claim	tests/lib/gutter-glyphs.test.ts, tests/ui/selection-action-summary.test.ts, workspace-comments-claim-verifier.test.tsx, doc-comments-panel.test.tsx, agent-ts/tests/claim-verifier-result.test.ts, thread-fallback.test.ts	tests/api/assistant-action-invoke-route.test.ts, claim-verifier-comment-migration.test.ts	tests/smoke/ai-factcheck.spec.ts, latex-selection-bubble.spec.ts
the contract	tests/ui/verifiers.test.ts (every built-in maps every verdict; unknown → pending; runtime registration)
this page	tests/ui/verification-doc.test.ts (every verifier, verdict and status; the identifiers, keys and kinds §8–§11 name)
enablement	tests/ui/use-workspace-verifiers.test.tsx (activeVerifiers, the hook and the rail's change event), tests/lib/claim-verdict.test.ts (the one claim grammar)	tests/api/workspace-modules-route.test.ts (verifies)

8. What each built-in is made of

§2 says what a verifier checks and how it answers. This is what it is built from — the columns that decide where its buttons appear and which module owns it. The drift test pins the identifiers.

	compile	lean (+ audit)	claim
Runner	Modal compile pool via /api/workspace/compile; the brain re-runs it after its own turns (runAutocompileIfNeeded)	Modal Lean pool via /api/workspace/lean/check for the check; a campaign of agent runs per formalization (Formalization: <file> seed chat, startFormalizationRun, then the legs in §8.1)	an agent run per claim (Claim Verifier chat, source: 'selection_action')
Module	none — built in (module: null) on .tex	lean4, lean-blueprint declare verifies: [lean, audit]	claim-verification declares verifies: [claim]; its action verify-claim names verifier: claim, result: thread, enabled_by_default
Gate	activeVerifiers (built in, .tex) + canCreateWorkspacePath(root)	activeVerifiers (enabled.has('lean'), .tex / .lean) → leanCheckProjectId	the installed, enabled action with verifier: 'claim'; owner/editor with write
Units it detects	the root .tex (resolveLatexRoot)	statements: listFormalizableStatements, paired by pairStatements	the same statement list, live whenever lean or claim is on (no Lean needed)
Result sink	tracked <root>.pdf + .synctex.gz files; per-line markers	the .lean sibling; <stem>.audit.json (audit); status.md	a doc_comment_threads row, kind = 'claim_verification'; verdict = the agent's message
Verdict grammar	CompileFailureKind latex / infra, stale	parseLeanStatements + #print axioms	one reader, lib/workspace/claim-verdict.ts (parseClaimVerdictLine), behind the glyph and the card; the agent writes the canonical line (claim-verifier-result)
Agent lane	latex_fix chat, fixLaneSystemPrompt, filterToolsForFixLane, blockedLatexCommand in the bash tool	formalize-selection (verifier: lean), search_lean_statements tool	the invoke route's annotation lane (result: thread), the verifier's resultInstruction, the thread authored as agent:claim-verifier; comment-delivery mirroring that fails closed
Model	fix lane on anthropic/claude-haiku-4.5	FORMALIZATION_MODEL (openai/gpt-6-astra) for the run chat; the manifest action's model for the selection action	the workspace default
Onboarding	SyncTeX tip card, the one-time auto-fix offer	five steps sorry → import → formalize → chip → share (sundial:lean-onboarding:<projectId>)	none
Persisted prefs	sundial:latex-autocompile, sundial:latex-autofix, sundial:latex-autofix-suggested, sundial:latex-scroll-sync, sundial:synctex-tip-seen, sundial:show-latex-format-bar, sundial:latex-workbench-editor-fraction	the onboarding key above	none (a BroadcastChannel for action toggles)

Beyond the five surfaces in §3, a verifier also reaches: the header cluster's width tiers (full · icon · minimal, where the verifier chips vanish) and the ⋮ menu rows; the selection bubble and its Customize disclosure; Monaco markers, statement highlights, the LeanStatusChip in every .lean editor, scroll sync; the companions' auto-open and idle fallbacks, the mobile LatexWorkbench; the gutter glyph and its card (in a code editor a claim's only annotation — no lane card, no span paint), ClaimVerificationThreadCard in the markdown lane and SelectionActionEventCard in chat, the hidden selection_action and latex_fix chats; and durable state — the keys above, files as storage (.pdf, .synctex.gz, .lean, .audit.json, status.md), workspace_assistant_actions and workspace_modules. Walk that list when you change one.

8.1 The formalization campaign

lean is the one built-in whose runner is a LOOP rather than a single run, so it needs its own paragraph. One Formalize press starts a campaign: a sequence of agent legs, each its own chat, driven by deterministic controller code in lib/formalization/campaign.ts. Agents never drive it; every leg prompt ends with the scope note telling the model to do its one job, report honestly, and never spawn a successor.

State. One row in formalization_campaigns (status, leg, last open count, dry legs, the current wave, the audit chat). A partial unique index allows one active campaign per project. Every transition is a compare-and-swap on state_version, so two racing workers cannot both advance.

Clock. The brain POSTs /api/workspace/formalization/advance when a leg's run reaches a terminal status (agent-ts/src/session/campaign.ts, fire-and-forget, shared secret). A lost ping costs nothing durable: sweepCampaigns, called by the brain's cron ticker every 60s, re-evaluates stale campaigns from observable message timestamps, re-enqueues dispatched- but-silent legs, and adopts orphaned seed chats. Dispatch is keyed (campaignWaveDispatchKey), so a retry resumes the same chat instead of minting a second prover against the same file.

Legs, in order. Translate (the seed chat) → align → prove → audit. Align is a blind back-translation (ALIGN_DECL, alignmentPrompt): a reader that never opens the .tex writes each declaration back as prose, then compares and fixes the LEAN statement where the two disagree, before any proving effort is spent on a statement that says the wrong thing. Prove is one declaration per leg (WAVE_SIZE = 1); parallel provers on one shared .lean poisoned each other, since a mid-attempt syntax error anywhere fails the whole file, so parallelism returns only with per-lemma file isolation. Audit is the terminal blind read-back that writes <stem>.audit.json.

Deterministic / not. Deterministic: the decision (decideCampaignStep is pure and unit-tested), the verdict (the Lean pool plus #print axioms, never the model's claim), the frontier (open declarations whose \uses{} ingredients are all closed, conjectures excluded by construction), and termination (goal met, DRY_CAP dry legs, or LEG_CAP; a cyclic cursor visits every frontier target before retrying one, and a rise in the open count counts dry immediately). Non-deterministic: only what happens inside a leg, the translation, the proof attempts, the decomposition, the read-back prose, the verdicts.

Refusing to guess. If the pool is unreachable the controller leaves state untouched and returns ok: false; the next ping retries. Missing evidence is never read as progress. The audit records sourceHashes.lean and sourceHashes.tex (SHA-256 of the exact source files). A refuted verdict can remove a declaration from scope only when both hashes still match; missing or stale hashes never produce a silent goal_met. The sweep also shares one route budget across the stale campaigns it verifies (SWEEP_BUDGET_MS, oldest-stale first), so one slow Lean check can't eat a tick and starve the rest.

9. Code map

compile — components/workspace/use-latex-compile.ts (the state machine), use-latex-autofix.ts, use-latex-fix-resume.ts, lib/latex/{autofix-guard,fix-prompt,fix-chat,compile-contract,synctex}.ts, lib/workspace/{latex-root,compile-pool,compile-ladder,latex-log-parser,latex-log-navigation,latex-monaco-markers}.ts, app/api/workspace/compile/route.ts, the viewer latex-pdf-viewer.tsx / latex-pdf-pane.tsx, the brain's agent-ts/src/latex/autocompile.ts, session/runner.ts (inline auto-fix loop), prompt/fix-lane.ts, tools/bash.ts. lib/workspace/latex-root.ts is mirrored byte for byte in agent-ts/src/latex/latex-root.ts; parity is test-enforced only.

lean and audit — lib/formalization/{detect,statements,graph,audit,run,onboarding}.ts, lib/formalization/campaign.ts (the controller, §8.1) with app/api/workspace/formalization/advance/route.ts and the brain's agent-ts/src/session/campaign.ts ping, plus the /api/cron/formalization-sweep tick, app/api/workspace/lean/check/route.ts, lib/workspace/lean-pool.ts, sandbox/lean_pool.py, components/workspace/{use-formalization-status,lean-status-chip,use-audit-verdicts,use-lean-onboarding,lean-statement-graph}.ts(x), FormalizeCluster in latex-editor-toolbar.tsx, agent-ts/src/tools/search-lean.ts, the manifests under templates/research/lean-blueprint and templates/project/lean4 (shared templates/_shared/lean4-setup).

claim — lib/workspace/claim-verdict.ts (the one grammar), lib/assistants/selection-actions.ts (the action shape, enabled_by_default, the invoke event; isClaimVerifierSelectionAction only renames legacy snapshots for display), lib/workspace/doc-comments.ts (DocCommentThreadKind), app/api/workspace/assistant-actions/invoke/route.ts (the two lanes, picked by the manifest action), app/w/[slug]/_components/workspace-comments.tsx (invokeClaimVerifier), lib/assistants/selection-action-summary.ts, agent-ts/src/claim-verifier-result.ts, agent-ts/src/session/thread-fallback.ts, ClaimVerificationThreadCard in doc-comments-panel.tsx, SelectionActionEventCard in ai-elements-transcript.tsx, templates/research/claim-verification/.

Shared — lib/workspace/verifiers.ts (this contract, activeVerifiers, recommendedVerifiers), components/workspace/use-workspace-verifiers.ts (useWorkspaceVerifiers: enablement from the installed modules), lib/workspace/gutter-glyphs.ts (mergeGutterGlyphs, claimGlyphs), latex-monaco-markers.ts (installGutterGlyphs), collab-code-editor.tsx (the merge, claim spans from thread anchors, the chip mount, the bubble).

10. Where the built-ins still disagree

The 2026-09-08 audit found nine seams; six closed the same day (identity lists → manifest verifies; the template-only Lean gate; Verify needing Lean; three claim grammars; the invoke route's identity fork; Formalize / Verify as toolbar props). Three stay open:

1. Two auto-compile engines (browser and brain), handshaking through holdAutoCompile / markBackgroundCompiled alone.
2. Three result sinks, three readers (files, threads, chat messages); the gutter is the only meeting point, through three adapters in collab-code-editor.tsx.
3. Per-slug copy and prop drilling: Lean / Graph empty-state strings, the Formalize title; leanCheckProjectId and onFixSorry still travel through SplitEditorPane into the generic code editor.

Loose ends, to fix as you touch the area: startWorkspaceFormalizationRun and startFaithfulnessAudit have tests and no caller (the audit writer is unwired, only its reader is); connected.formalizable is computed and never read; assistantGreeting is always empty; /docs/modules says removing a module deletes its files (the route keeps them); the sidebar's canManage={canWrite} is looser than the server's owner-or-editor rule; no smoke exercises a Lean surface end to end.

11. Module ownership: the manifest

A module owns its verifiers in its manifest; the page asks the registry which apply.

# manifest.yaml
verifies: [lean, audit]          # registered VerifierSpec ids this module switches on
selection_actions:
  - id: formalize-selection
    verifier: lean               # the verifier whose verdict this action produces
    model: openai/gpt-6-astra    # the run chat's model
  - id: verify-claim             # (claim-verification's)
    verifier: claim
    result: thread               # the answer annotates the selection
    enabled_by_default: true

// what the page asks
const { enabled } = useWorkspaceVerifiers(projectId);          // from GET /api/workspace/modules
const specs = activeVerifiers({ path, enabled });               // built-in ∪ enabled, filtered by documents
const chips = specs.flatMap((s) => renderers[s.id]?.() ?? []);  // LatexCompileControls verifiers={chips}

The invoke route reads the same manifest action: result: thread with a verifier → the annotation lane, the thread authored agent:<id>-verifier with the verifier's label, the verifier's resultInstruction appended to the prompt; otherwise a chat on the action's model.

Still to do, in the order that pays first: the /docs/modules trigger vocabulary (compile, change) as manifest on: entries; one adapter for the three result sinks (§10.2); retiring the gallery's and the onboarding's per-slug module tables once the manifest carries a kind.