Verification

How the workspace answers “is this right?”: one contract for every verifier, five shared statuses, the same surfaces for each, and evidence one click from every status. Kept in step with the code by a test.

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
  speed: 'hours',             // SPEED_WORDS: how long one run takes
  offer: (n) => `I’ll write ${n} theorems in Lean and try to prove them`, // Sunny's first-person offer
  cost: { per: 'try', micros: LEAN_STEP_COST_MICROS, upTo: 32 }, // free | check | fact | try (at most upTo tries)
  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
  onSelection: true,          // the text bubble offers it on a selection: true = its module's selection action, a string = its popup's event (a built-in)
  selectionDocuments: ['.tex'], // where the bubble offers it, when narrower than documents (a .lean selection is Lean already)
  resultInstruction: '…',     // for an agent-written verdict: the output contract every reader parses
  runsOn: { model: 'openai/gpt-6-astra' }, // a model the workspace can pick (default here; null = a new chat's), or { engine: 'Pangram' }
  madeBy: 'Written with',     // the quiet line under a result: "Written with GPT 6 Astra · 3 credits"
});

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:

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.
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.
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.
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 builds (every settled edit with auto-compile on; the plain ▶ otherwise) never fix; Fix my LaTeX (the launcher, the status chip) builds, fixes as suggestions, builds again	`compiled` ok · `warning` warn · `error` error · `stale` warn · `compiling` pending	header chip (▶ + 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 · `refuted` error	header chip (verdict first, "Proved · 4 checked"), `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	its card beside the sentence in the comment lane (on a `.tex` as on markdown: Sunny, the fact, Fix it · See the work · Dismiss), the sentence's wash in its status color in the source and a quiet tint on the PDF, the verification thread and its chat; no line glyph
`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
`ai`	the selected writing, or the whole document — how much reads as AI-written (Pangram); past the detector's 40,000-character cap the whole document reads part by part, one check a part, in as few parts as fit, cut between paragraphs where that costs no extra part (`pangramParts`, merged back into one answer by `mergePangramParts`); Try again re-reads only the parts not yet answered. A selection past the cap is refused, as nothing on the bubble counts parts	manual (the text bubble's AI check on a selection, or the launcher's AI-written? on the whole markdown doc: `sundial:open-pangram` with `{ whole: true, source }`, where `source` is the one editor's `view.dom`)	`human` ok · `mixed` warn · `ai` warn	cards in the document's comment lane, like Is it true?'s (`components/workspace/editor-ai-check.tsx` runs the check; `lib/workspace/ai-check-cards.ts` holds the cards; `AiCheckThreadCard` in `doc-comments-panel.tsx` draws them): one summary card for the checked range ("AI-written? · Whole document · 26% AI", Pangram's AI fraction, always a percent AI, never a percent human, plus "And 12% reads partly AI." when Pangram read some as assisted) that names the detector ("Checked by Pangram" with an eye; its hover and click say how Pangram works and that it can be wrong), and one card per window (`readWindows`) that reads as AI or partly AI, named by its span ("Paragraphs 2–5", `spanWords`) with the window's own score ("76% AI") and verdict. Human windows get no card. Flagged words wear a dotted orange underline (never a fill, never on a heading or code), lit while their card is hovered or selected; selecting a summary lights every word its run marked and scrolls to the first, and a click in flagged words selects its card without scrolling. Every card sits beside where its words start (the lane centers a card on at most its range's first lines). The newest answered check on some words speaks for them (`newestAiCheckWins`): an older card's underline stops where a newer selection check read, and an older card it read entirely steps aside, while a check still reading or one that failed hides nothing and is never hidden. Checks on a file read one at a time, in any pane (a second selection check says "Another check is still running. Give it a moment." with Try again; a whole-document check replaces the rest), and every answered card, saved or not, is dated by its last answer on the server's clock (its receipts; never later than its saving). Every answered card in the document's lane offers Check again (`sundial:ai-check-again`, claimed by the first editor showing the card's words): a window or selection re-checks its words now, a whole-document summary the whole document; while another check on the doc reads it says so instead, and a Check again that starts nothing always says why. Typing while it reads is fine: each flagged part is found again by its own words, nearest where the edits moved it (so typing, moving a paragraph, an undo or a collaborator's edit all keep it), and only a part whose own words changed goes unmarked (the summary says so). One window over everything checked gets no second card: the summary sits on its words and wears their underline (a one-paragraph selection, a short page), and over several paragraphs says "I read all of this as one piece.", plus "Select one paragraph to check it on its own." when a paragraph is long enough. It only finds: nothing offers a rewrite. The cards are a thread kind (`ai_check`): while a check reads they live for the session, by workspace and file (`aiCheckFile`), and a check still reading or failed goes with its editor; once it answers they are saved as comment threads (`saveAiCheckRun`: one `POST /api/workspace/comments` with `kind: 'ai_check'` and the run's cards; the thread is the module's, its message records who saved it (a signed-in or anon-cookie visitor with suggest access; 401 otherwise), no agent summoned; the card rides in the message, words first, then a `sundial:ai-check` marker, `lib/workspace/ai-check-saved.ts`), so a reload and collaborators see them, a new whole-document run retires the file's earlier ones (`replace`, only for a saver who can write the file, the same rule as resolve), the saved threads the save answers with take the session copy's place at once (a run dismissed while it saved has them resolved), and Dismiss on a saved card resolves it (a summary takes its windows with it; shown only to a reader who can resolve; no History event). Until migration `20260930230000` lets the kind in (it also lets in `stale_check`, for Out of date?), the save answers 409 `kind_not_ready` and the cards stay session-only
`stale`	one sentence against the OTHER files in this folder (Out of date?, the `out-of-date` module): does another file say something different, and is it newer by last edit? Never the web, never which file is right; comments, chats, other checks' cards and `skills/` are not evidence	agent (the text bubble on a selection, or the launcher's Out of date? on the whole page: the same split, heads-up and queue as Is it true?, keyed by its id)	`newer_file` warn · `other_file` warn · `consistent` ok · `failed` warn · `pending` pending	its card beside the sentence in the comment lane (the same card as Is it true?'s, read by thread kind `stale_check`): "A newer file says otherwise" and a reason naming both files and their dates ("results.md (edited Sep 28) says 71%; this says 64%"), See the work · Dismiss; the sentence's wash; a page with nothing to flag says "Matches your other files · 5 checked"; no line glyph

What the student sees. Each spec carries its own words, and every surface (tour, launcher, rail, text bubble, cards, popups) reads them from the registry, never from a string of its own: label is the name (compile Fix my LaTeX, lean Check with Lean, claim Is it true?, audit Matches the paper?, ai AI-written?), pitch the one sentence of what it checks, speed (SPEED_WORDS: A few seconds, About a minute, A few minutes, Can take an hour or more) how long a run takes, offer what Sunny says it will do, in first person, for a count ("I’ll check 6 facts on the web"), cost what a run costs (free; a flat check; one agent turn per fact; one per try of a many-run check like Check with Lean, whose micros are a measured median and upTo the most tries a run can take: the seed, LEG_CAP legs, the audit), running the words while it runs, part (optional) the words while a long document is read part by part ("Reading part 2 of 3…"), says the words for each verdict (verdictWords(id, verdict)), and failed what a surface says when the service behind it can't answer, by why (failureWords(id, why)), never an endless running line. Only unreachable ("Couldn’t reach Lean.") sits next to a Try again; too_big, not_set_up ("isn’t set up here yet") and refused would fail again, so they offer none. The verdict words themselves stay the verifier's own, so old results still parse. Each check also has a face: sunny is Sunny's pose while it works (compile laptop, lean grad, claim search, audit book, ai telescope), and SUNNY_REACTION is how Sunny reacts to a result (a hop for ok, a shrug for warn, unrolling a scroll for error, never a check's own working pose); a run that could not finish is SUNNY_OOPS, never a verdict. A label names the whole job, not its first step: Fix my LaTeX builds the PDF and, when the LaTeX has errors, Sunny fixes them as suggestions you can accept; Check with Lean names the checker.

Fix my LaTeX is one flow (components/workspace/use-latex-fix-flow.ts). One click on it (the launcher) builds the PDF. A clean build says so ("No LaTeX problems · PDF up to date", Sunny's reaction). A build with errors goes straight to Sunny, no second click: the fix turn goes to the project's latex_fix chat in suggest mode, so every fix lands as a suggestion on the .tex that the student accepts or rejects inline (the same review marks agent edits use; each suggestion's author chip opens the fix chat, "See the work"). When the fix run ends it builds again to check ("Fixed 2 LaTeX errors · Accept or reject each fix", or "1 LaTeX error left"). While it works one running line says the phase with one clock from the click: "Building the PDF…", "Fixing 2 LaTeX errors…", "Checking the fix…" (the header, the status popover in place of its button, the launcher item). The status chip's Fix my LaTeX, Cmd+Enter in the editor, the error hover's quick fix and a sign-in resume join the flow at the fix step, from the errors on screen. Automatic builds (on open, after a pause, after an agent's edit) stay quiet and never start a fix; after one with errors, the status chip offers Fix my LaTeX as its one primary. The plain ▶ in the header is editor chrome: it builds, never fixes, and its tooltip says "Build the PDF". The answer describes the build it read: the next build, automatic or plain, drops it. Opening a non-LaTeX file mid-flow only pauses it (Sunny keeps fixing; the check runs when the .tex is back); another LaTeX root ends it. Whoever can't build sees Fix my LaTeX greyed with the status chip's words ("Sign in to compile", "Read-only access"), and See the work opens the fix chat beside the student's own.

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 compile error): the worst status wins, then the higher glyphRank (Lean 3, compile 2); the rest ride along on the card. A checked sentence on that line keeps its own card in the lane.
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.
A check that can't start (signed out, out of credits, not set up on this server): the card or popup shows the one wall every editor AI tool shares (components/workspace/cant-start.tsx), with the button that fixes it — Sign in opens the sign-in modal, Get more credits opens Sunny's credits card (below). Never a bare error with only Close.

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: the plain ▶ build with the compile status (its popover offers Fix my LaTeX), Check with Lean (Check with Lean · n before a sibling exists, then verdict first: "Not proved yet · 1 of 4"), Is it true? (no count: its press finds the real one), 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), status is the color (green, hollow green, orange, red, hollow). On a line with several, the worst status wins and Lean ranks over compile; the rest ride along on the card (mergeGutterGlyphs). Is it true? draws none (glyph: false): one anchor per statement, and a checked sentence's anchor is its card.
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), 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 my LaTeX 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. A fix is a paid run, and the compile status popover opens by itself over the text: its Fix my LaTeX takes a click only once the popover has been up a moment (twice FIX_SETTLE_MS) and, for a mouse, the pointer has moved onto the popover and rested (FIX_SETTLE_MS; a move is told by position, as WebKit reports no movementX; a touch has no hover); any other click only closes it, like a click outside. Keys always work.
Margin — the claim cards live in the comment margin, beside the source on a .tex exactly as on markdown (the same ClaimVerificationThreadCard; the sentence wears its verdict's wash in Monaco, .monaco-comment-range-claim). A page whose claims have verdicts opens with the margin showing (useWorkspaceComments), never a sheet on a phone; a student who closes it keeps it closed in that tab until they open it again.
Live step line — a check an agent runs shows what it is doing right now, in Sunny's words ("I’m reading nasa.gov…", sunnyStepWords in lib/workspace/sunny-steps.ts), with a clock (<Elapsed>, one shared 1 s ticker). The wire: while a comment or formalization run works, the brain stamps its latest step as metadata.step ({ tool, path?, url?, query?, command?, at }) on the in-flight assistant row (agent-ts/src/session/step-stamp.ts: at most one write per 2.5 s, only while the row is still that stream's streaming row, never awaited). A step is stamped when it STARTS (createStepReader): a tool call on its first chunk, its file as soon as the streamed input names it (so a minute-long write of paper.lean reads "Writing paper.lean…" from the first second), and tool: 'thinking' ("Thinking…") when a model step has no tool yet. No label is keyed on setup.sh: it is seconds of plain code. The workspace's chat-status realtime channel (and its reconciler, after a reload) passes it through liveFromMessageEvent into a per-chat store (lib/workspace/chat-steps.ts), so a step re-renders only the card or row showing that chat. The claim card puts it under its name (the announced live region says only the start and the answer), the Verify chip reads Checking n… with the clock (a click then opens a running check's chat, never a second batch), the launcher and rail rows add the clock, the rail's hover says the step. A run that died says why (sunnyFailWords: "I ran out of credits"). A check can phrase the step itself (live.say, read per chat by <LiveWords>): Check with Lean reads its campaign's live chat (liveCampaignChats knows the seed, "Align statements: …" and the provers) and says the phase (campaignPhaseWords in lib/formalization/run.ts): "Writing paper.lean…", "Checking the Lean says what your paper says…", "Proving Lemma 3 (try 2)…" (tries count only this run's provers). Every running surface points at that chat; a statement's glyph only at its own prover (campaignChatFor). Before a start, its hover says what the scan found ("Found 4 theorems and lemmas in paper.tex", foundWords in lib/formalization/detect.ts).
Sunny — each check has a face (sunny): its working pose animates on ONE surface per run (useSunnyLead: the selected card, else the first running card, else the header chip), every other one shows the ~10 KB still. A result plays SUNNY_REACTION[status] (a failure SUNNY_OOPS) once, only when that surface saw the run finish (useSunnyReaction, two at a time page-wide), then rests on the still; a card that mounts with its answer never reacts.
Before you start — before a click, a check says what it will do, how long, and what it costs this person, in Sunny's voice: beforeYouStart(id, ctx) → offer · speed · cost, e.g. "I’ll check 6 facts on the web · about a minute each · you have 3 free checks, so I’ll do the first 3". The cost clause follows the claim-split budget exactly, so the preview never promises what the click won't do. A document's count is its paragraphs, an estimate (the split can cut one into several facts), so a batch promises per fact; only the bubble's one selection (exact) is an exact count. An anonymous visitor's agent runs come out of their free runs ("one free check a fact, 3 left"; for one selection "uses 1 of your 3 free checks"; "your free checks are used up, so sign in first"); a check that is not an agent run (AI-written?), or takes many runs (Check with Lean: "it takes several runs, so sign in first"), asks to sign in first; a signed-in batch is max(1, floor((balance − held) / turn)) turns, the same arithmetic as reserve_credit_batch, where held is what recent batches' live reservations still set aside for 15 minutes, and a turn is the measured p90 of a fact check (ESTIMATED_TURN_COST_MICROS, $0.35: "up to 4 credits a fact", "up to 4 credits a fact, enough for 6", "you have 20 credits, so I’ll do the first 5", "some credits are still set aside for your recent checks, so I’ll do the first 8"). When the student's own Claude plan pays for fact checks (plan, which GET /api/workspace/claim-split?projectId= names before any press and each split answer refreshes, carried in the budget), credits are not the question: the cost clause is "Claude plan connected" (PLAN_WORDS), and nothing is set aside. A cost the page can't know (balance, holds or the network's ceiling not read yet, metered billing) is left out, never "0 credits". Free runs are both keys the gate checks, the smaller wins: the visitor's own (anonRunsRemaining) and the network's rolling ceiling (anonIpRunsRemaining, which a shared campus network can use up), both on the files payload and its SSR preload. The context is those counts plus the page's one billing read (useCreditSummary, whose summary carries heldMicros; shared with the low-credits pill and re-read when a claim batch settles), turned into a budget by verifierBudget and handed to the bubble and the tour through VerifierBudgetContext (lib/workspace/verifier-budget.ts). It is a preview: the click's notice stays the authority (a key of your own can make a zero balance run).
A long page — Is it true? finds EVERY fact on the page before it checks any: the split reads the whole document (up to MAX_CLAIM_SPLIT_CHARS, a million characters, so a 100-page paper is read to its last page), cut into ~5k-character parts (passageParts) listed side by side, 16 at a time, each retried once. A LaTeX paper's theorem and proof environments are cut out first (withoutProofs): its mathematics is Check with Lean's job. The answer is the exact list in reading order, minus what earlier presses checked (checkedClaims, sent as checked); total is that list's length plus the checked ones, never the model's own guess (it guessed 284 on a page of about 90), and unknown when a part failed. Check every fact (lib/workspace/fact-queue.ts): pressing Is it true? on a whole document first finds every fact, marks each with a quiet grey dotted underline (sd-fact-found: setFactMarks in lib/tiptap/fact-marks.ts on markdown, the code editor's markFacts on LaTeX and text; a mark goes as its card lands), and says one heads-up before anything paid (factHeadsUp, a waiting check notice with one CHECK_PRIMARY and a row of CHECK_LINKs). Its numbers are the split's real count and the measured cost: "about" the median fact (TYPICAL_TURN_COST_MICROS, $0.27), "at most" the p90 (ESTIMATED_TURN_COST_MICROS), exact under 20 credits, then to the five, from 100 to the ten.
- Enough credits: "I found 90 facts. Checking them all uses about 240 credits (at most 320). You have 480." Check all 90 · Just this section · Not now. Just this section is the facts between the heading above the caret and the next one of its level (headingSection, textSection), offered only when it holds some but not all.
- Short on credits: "I found 90 facts. You have 60 credits, enough for about 17." Check the first 17 · Get more credits · Or use your Claude plan. With none at all, "You’re out of credits." and only the two ways to pay.
- A connected plan: "Claude plan connected · 90 facts" and just Check all 90. The student's own API key: "Your own API key pays for these." A plan or own-key payer at a zero balance still gets the split (it costs cents, metered; the route answers ownKey). When the split fails, the list is the page's prose paragraph by paragraph (a paper's theorems and proofs blanked, blankProofs), and the heads-up says so: "I couldn’t pick out single facts, so I’ll check the 40 paragraphs." Past MAX_CLAIM_SPLIT_CHARS it adds "It’s a long document, so that’s from its first part." A signed-out visitor: "You can check 3 for free." Check the first 3 · Sign in to check them all. A page pressed again says what is left ("20 facts left to check."). The heads-up holds nothing: the split's first-batch reservation goes back (PATCH) as it shows. The queue (runFactQueue) then checks MAX_VERIFY_CLAIMS (12) at a time, one run each, in reading order: each batch reserves its own credits as it starts (PUT /api/workspace/claim-split, { projectId, units }, through the same gate; a visitor's batches count down their free runs), captures its facts as they are then (a fact edited away starts nothing, and gives its credit back), and waits until its cards settle (batchStillRunning: open cards that were not on the file when the batch began, by id, unanswered, whose chat has not ended; read from the server each look, so a quiet live feed never ends a batch early), then gives its reservation back (BatchAllowance.release, PATCH to 0: its turns have debited, and a held batch would count twice against the next) before the next. While it runs, the rail row, the launcher and the notice say how far it got (factProgressWords: "24 of 90 checked · 3 look wrong so far"), the notice with Stop, read between batches (a check already running finishes). The row stays live between batches, so no batch's finish notice cuts in. An end short of the last fact says so (factEndWords): "Checked 70 of 90. You’re out of credits." with Get more credits and the own-plan link (and the credits card pops, below), "Checked 3 of 90. Sign in to check the rest.", "Stopped at 24 of 90. Press “Is it true?” again to go on."; checking them all ends on the usual finish notice. A short end swallows only its own finish notice; once that edge has passed (or on a file switch), a later claim notice, the text bubble's among them, speaks again. Pressing again while the queue runs brings its progress back; after it ends, a press resumes: the split skips every fact with a card (checked), so only the rest are found, counted and offered. A press while checks still run here (a text bubble's, a batch's) starts nothing and says "Still checking 3 facts…" (noNewFactsWords, which also words "All checked" and "No facts to check here"). A later press starts no more than the split counts left (factsLeft): told what is checked, the model may pad a finished page with sentences that aren't facts. An answer cut off at the output limit keeps the entries before the cut. A selection (the text bubble's Is it true?) is one fact, as before: no heads-up beyond its hover line. On a markdown page the split reads each block's text with a hand-wrapped line break as a space (listTextblockRanges), and a returned fact is found with the same convention (findQuoteRange(editor, quote, ' ')), so "on a" + "Usenet" never reaches the model as "on aUsenet".
What a fact check reads — only outside sources count as evidence. The turn a one-click check starts (isClaimVerificationTrigger) runs the fact-check lane (factCheckLaneSystemPrompt, filterToolsForFactCheckLane in the brain): a short fixed prompt with no workspace instructions, module notes or skills list, and only the web tools. The student's other files, notes, chats and earlier checks are never evidence (they may repeat the same mistake); the paragraph only says what the sentence means, and what comes before it (claimContext's before: the page's title and author lines, then the nearest blocks above, whole, up to ~800 characters) only says who “I” or “we” is. The check judges the claim about that person, never that it can't tell who “I” is. The invoke route puts the bibliography entries the sentence cites (citedEntries: a \bibitem, a .bib record, a markdown footnote; a rendered sentence's keys come from its own source sentence, never a neighbour's) into its message, so it never opens the paper; Read exists only when the sentence names a workspace file (citedPaths), pinned to that file. The Claude and ChatGPT plan harnesses get the same prompt and tools (resolveTurnConfig); there the harness's own preset (Claude) stays, so the prompt is the guard, and the Codex CLI runs read-only in an empty folder (workdir: "empty"), never a shell on the student's project (it still boots the workspace sandbox, and could read a file by its full path). A follow-up in See the work gets the full Sunny prompt back, plus a short note naming the card (checkFollowUpFor, prompt/check-follow-up.ts): when the answer settles the claim differently, or the student asks for a re-check, the reply opens with the result block, and restateCheckVerdict posts its line on the thread, so the card moves (never for a failed turn, a guest turn, or one that edited). A ChatGPT plan never pays for a check (resolvePlanRuntime): it runs only through the Codex engine, one turn per person at a time, so a page of facts would wait in line about a minute each. Checks stay on credits.
What Out of date? reads — only the other files in this folder, never the web. Its registry entry says lane: 'folder', so the invoke route puts a dated index of the folder in the run's message (folderIndex, lib/workspace/folder-index.ts: every other file with its last edit, newest first, each marked newer or older than the selected text: when it was written, from the markdown blame lens (sentenceWrittenAt), else the checked file's own last edit, said as such; skills/ left out; a failed folder read stops with 502 before anything is charged) and stamps lane: "folder" on the trigger. The brain runs that turn on the Out of date? lane (isStaleCheckTrigger, staleCheckLaneSystemPrompt, filterToolsForStaleCheckLane): a short fixed prompt, Read, Grep and Glob only, the execute guard refusing everything else; the Claude harness drops its WebSearch/WebFetch and the OpenAI one its hosted web tools for it, and the Codex CLI runs read-only with web_search="disabled" (the body's web_search: false). The card's one line is canonicalized like Is it true?'s (staleCheckCommentBody, agent-ts/src/stale-check-result.ts) and read back through the registry's verdict words (parseVerdictText). Its thread kind waits for migration 20260930230000; until it lands the invoke route answers 409 kind_not_ready ("Out of date? isn’t ready here yet") and leaves nothing behind.
Never ran — a check that never ran here never says it is working: the Graph leaf of a paper with no .lean and no live Check with Lean run keys its statements "Not checked yet", with no "Checking with Lean…".

Where each surface reads a check's words (all from the registry, never a string of its own; tests/ui/verifier-names.test.ts fails when one spells a name itself):

Launcher (the orange tab, launcherItems in the workspace page): each check's row is its label, its hover line (the black label beside the column) its before-you-start line (a reason it can't run wins over it). While it works the row says its running words and a clock, and a click opens the work; it is never greyed. In a folder on this Mac, where no check runs, each check whose module's skill is there (folderChecks) is greyed with FOLDER_CHECK_WORDS; Customize's Add more (addableChecks) lists the checks not added yet and adds them the way the rail's + Add does (the hover says where they run).
Header chip: Is it true?, with no count (a paper's sentence count is not its fact count; the press finds the real one), shows the same before-you-start line on hover (LatexVerifyState.before), per fact and with no count to promise, since the heads-up says the real one. AI-written? is a row on a markdown doc: it dispatches sundial:open-pangram with { whole: true }, the whole document, answered in the comment lane as a selection is (the lane opens for a new check, even one closed on purpose). Its before-you-start line counts the document's parts (useAiCheckParts, re-counted once typing pauses): "I’ll read this in 2 parts and guess how much reads like AI · a few seconds each · less than a credit a part".
Rail row (VerifierRowView): the label, the pitch on hover, a quiet mark that glows while the check runs (never a verdict color), and a summary for the open document in plain words ("3 theorems, not checked yet", "2 of 3 proved", "3 checked · 1 disagrees", "Needs a LaTeX file"). A summary reads clean ("No problems found", "all match") only when every verdict is clean (lib/workspace/verifier-summary.ts): a hedge, a run that died or a partial match is named, never passed off as a pass. In a folder on this Mac the summary is FOLDER_CHECK_WORDS ("Only in a Sundial drive for now") and the row has no ⋮.
Text bubble (SelectionChecks, the same on every file: the markdown editor's EditorBubbleMenu and the code editor's CodeSelectionBubble): exactly the checks that run on a selection, then Comment, then (markdown only) an emoji reaction, and nothing else (no formatting, no Ask, no AI tools, no Customize; formatting stays on the menu bar and its shortcuts, ⌘G still opens a rewrite). selectionChecks(path, actions, events) picks them: every check with onSelection that applies to the file, in registry order (the launcher's), each with its Sunny still and its label, its before-you-start line for one fact on hover, or the wall's words (WALL.credits once out of credits, WALL.signin when needsSignIn). A module's check (onSelection: true) shows while its module's selection action (verifier: <id>) is installed (installed is on: there is no switch, as in the launcher, and the invoke route runs any installed action; the manifest's enabled_by_default only sets the stored flag at install), and runs through it on the selection alone; a built-in names its popup's event (onSelection: 'sundial:open-pangram') and opens it on a captured selection, so a host that cannot capture for it (the code editor) leaves it out. selectionDocuments narrows a check's files for the bubble alone. A .md selection gets Is it true? and AI-written?; a .tex one Check with Lean and Is it true?; a .txt, .rst or .org one Is it true? (PROSE_DOCUMENTS, claim's selectionDocuments, which the launcher's "Open a document to check" reads too); a .lean or code file none, only Comment. The host reads the list (useSelectionChecks) and stays mounted while the bubble comes and goes, so a selection paints its whole row at once; with no check and no Comment (a read-only diff or Lean pane) there is no bubble. Fix my LaTeX and Matches the paper? stay launcher-only: each judges a whole document (one build, one .tex against its .lean), so a passage has no verdict of its own.
Tour (TOUR_CHECKS, lib/onboarding/tour-script.ts): the picker is the registered checks with their label, SPEED_WORDS and, under it, what a pick costs you (beforeYouStart(id, ctx, 'cost'), the whole line in the black hover label). Logged out, "run one" names only the picks that can start without an account (needsSignIn: Fix my LaTeX always, Is it true? while free runs last, never AI-written? or Check with Lean); none → Sunny says so and skips ahead. After the checks come the modules that are not checks (TOUR_MODULES, e.g. Citations): their own pitch as the hover, no speed or cost, and never counted as a check to try. "Go with N" installs each pick's module through the rail's add path (connectWorkspaceModule), and the tour celebrates only when a picked check really starts, never on a click: the surface that runs it calls announceCheckStarted(id) (lib/workspace/check-started.ts) once its request went through — the Claim Verifier's invoke answered, the AI check's detector took the text, a Lean run was created, a Fix my LaTeX the student asked for began. A refusal (signed out, out of credits, too short) or an automatic build never counts.

One look

Every check looks the same at every step, on every surface. The kit is one file, components/workspace/verifier-rows.tsx (plus useRunSince in elapsed.tsx and FailureNote in cant-start.tsx); tests/ui/check-visual-kit.test.ts fails when a check surface brings back a banned look (purple or indigo, spinners, ping dots, shadows, uppercase, solid black buttons, amber).

Status mark: StatusDot is the only status mark on one-line surfaces (launcher item, header chips, Lean chip, statement lists). The rail is the exception, and calm: its RailMark is a plain stone dot (an empty ring for a check not added) that glows softly (.sd-check-glow, steady under reduced motion) while its check runs. Filled for ok / warn / error, hollow for conditional / pending. While its check runs (running) the dot is a hollow orange ring with a gentle pulse (still under reduced motion), never a verdict color until the run settles. The gutter glyph and graph nodes keep their shapes.
Sunny: CheckSunny shows the check's registry pose while it works (the step's pose once there is a step), animated only on the one surface that leads the run; the oops pose when it failed or stopped; the reaction once, on a surface that saw it finish. The still is painted under the sprite, so Sunny is never blank.
Running line: RunningLine is the running words (or Sunny's latest step), the progress ("1 of 6 done") and a clock that counts from the click (useRunSince). In a chip it is the same content inline (RunningChip in the LaTeX toolbar). No spinners, and speed words only before the start.
Start: the click puts every surface of that check in its running state at once, and keeps it there until the run is seen live (never back to idle while the chat is created or the cards land). A check slower than seconds raises one flat check notice with its Sunny ("Checking with Lean… Can take hours."); a follow-up replaces it. A start never opens a chat; See the work does.
Result: ResultLine on cards and popups (the verdict words in the status color, the reason under it), StatusDot plus stone words on one line. Batch words are verdict first: "A source disagrees · 2 of 6"; a check with a long name (Matches the paper?) puts the count first on the rail, so truncation keeps it.
Actions: at most one CHECK_PRIMARY (the soft orange next step: Fix it, Try again, Prove, Sign in, Get more credits) per surface; everything else is a CHECK_LINK. A check's trace is always "See the work".
Failure: FailureNote (oops Sunny, words, one CHECK_PRIMARY) for a check that can't start or couldn't finish; a run the student stopped says "You stopped this one" at once (any other end says "I couldn't finish this one"). Out of credits is the same on every check (WALL.credits): "Get more credits", or "Or use your Claude plan" (Settings, API keys). A ChatGPT plan never pays for a check.
Out of credits — Sunny's credits card (components/workspace/credits-modal.tsx), on the tour's welcome card (CARD, the desktop handoff's too). It pops by itself when a page of facts runs out partway, when a press or a start is refused for credits (the split, the bubble's check, a Lean or LaTeX run), and from every Get more credits (askForCredits, GET_CREDITS_EVENT). Sleepy Sunny; "I checked 12 of 40 facts. Add credits and I’ll check the other 28."; a bar of what is checked and how far the picked top-up would go ("$20 checks the rest"); $5 / $20 / $50 tiles with their credits and about how many facts each covers (factsAffordable), the smallest that checks the rest picked; one primary, "Add 200 credits for $20", straight to the same Stripe checkout as Settings ▸ Billing (startCheckout); Monthly plans · Use your Claude plan · Not now. Checkout comes back to the page (?checkout=, checkoutReturn) and the card with it: after a payment it waits for the credits to land (the balance read every 2s, "Thanks! Adding your credits…"), then dances with confetti: "Your credits are in! Want me to check the other 28 facts?" Check the other 28 runs them (opening the file they are in first) with no second heads-up when the balance covers them. A cancel brings the same card back.
Finish: a check slower than seconds that the page watched run raises one check notice once every answer is in (checkEdges): Sunny's reaction, played once, the batch words and See the work as a link. Never on load or a file switch, and never for a stop or a failure.

The Checks page

Every module run in one place (Belinda 2026-09-30: "see all of the verifier runs that have happened in one place… open the traces from there"): a center leaf, checks (sundial-checks://all, or one module's sundial-checks://<id>; docs/view-sdk.md), opened by the Modules header's See all and each check row's ⋮ See all runs (already filtered to it). Filter words at the top: All and each registered check's label. One row per run, newest first and running ones on top (components/workspace/checks-view.tsx, in the kit): the check's CheckSunny still (glowing while it runs), its name, the document, the text it checked (one line), when, the result in words (the verdict's says plus a detail such as "82% AI" or "3 suggestions"; never a colored dot), and See the work. The row opens the document at the checked text; See the work opens the run's trace beside it, the same one its card, suggestion, finish notice or graph node opens: a Fix my LaTeX fix's turn in the fix chat, any other run's chat, an AI-written? result's saved card. A run whose thread was resolved or dismissed (resolved) and has no chat has no See the work: the lane no longer shows it, so the row's words are its result. When some module's runs fail to read (the route's failed), the page says "Some runs couldn't load. Try again" above the list.

Rows come from GET /api/workspace/checks?projectId in one shape (CheckRun, lib/workspace/check-runs.ts). Where each module's runs come from is one reader per module, keyed by its id, in lib/workspace/check-runs-server.ts (CHECK_RUN_READERS); the route asks every registered check for its runs, and a new check adds its reader there and nothing else. Today: Is it true? and Out of date? = their card threads (the registry's thread kind: claim_verification, stale_check), open and resolved; AI-written? = its saved summary cards; Fix my LaTeX = each turn of the fix chat, with how many suggestions it left; Check with Lean = each campaign (its seed chat is the trace, its provers its tries), each of a campaign's tries ("Prove: …", "Align statements: …", on its paper, so every prover's chat stays reachable) and each run chat no campaign owns; Matches the paper? = each campaign's audit (its saved verdicts in batch words) and each audit started on its own. Every query is bounded. Anyone who can read the workspace reads it: a guest on a file or folder link sees only runs on paths they can read, with no traces; a member who can't write sees the traces the Chats list shows them (nonWriterSeesChat, shared with the chats route: every chat on a workspace-root link, else the ones they take part in or made).

Chats is for talking, Checks is for runs. A check's run chat leaves the Chats list (isCheckChat, read by shouldShowSelectionActionChat): a fact check's selection_action chat, the latex_fix chat, and the Lean and audit chats, which are tagged kind: 'check' when they are made (lib/formalization/run.ts createRunChat, campaign.ts dispatchRun), older ones known by title (CHECK_CHAT_TITLES: "Formalization: ", "Prove: ", "Align statements: ", "Faithfulness audit: "). The one that is open still shows, and every one is on the Checks page. Only where that page exists: in a local-folder workspace or on a phone (no Checks page) only selection_action chats hide, as before.

Starting a run without a click

Sunny and outside agents start a module exactly as its one click does: POST /api/workspace/modules/run with { projectId, module, path } (app/api/workspace/modules/run/route.ts). It checks the caller may edit the workspace (a viewer is read_only, a signed-out visitor signin_required), that the module is added (a catalog module's verifies; a built-in always is), the file exists and is a type its starter takes, then runs that module's starter from lib/workspace/module-starters.ts (MODULE_STARTERS, one per module id). A starter calls the same routes the click calls, in-process and as the caller (lib/workspace/route-caller.ts: their cookie or Bearer token, their abort), so the same auth, run gate and credits apply and the results land where a click's do (the fix chat's suggestions, the lane's cards, a run chat) and on the Checks page. Fix my LaTeX builds (free) and sends a fix turn to the one fix chat only on LaTeX errors; AI-written? reads a markdown file part by part and saves its summary card; Is it true? splits the facts, starts one check per fact up to the split's budget (anchored by quote) and gives back what it did not start; Check with Lean and Matches the paper? start their run chats (lib/formalization/run.ts).

The answer is { module, path, summary, verdict?, chatId?, threadIds? }, summary one plain sentence. A refusal is { refusal, error } with its status (REFUSALS): account_token_needed, signin_required, out_of_credits, read_only, workspace_not_found, unknown_module, module_not_added, file_not_found, wrong_file_type, too_short, busy, not_set_up, failed. Auth is a session, an sd_ token or an anonymous owner's cookie; a workspace join token (what /g/compile takes) is refused, since the routes behind a run accept none.

Sunny's tool is run_module (agent-ts/src/tools/run-module.ts, acting as the person who asked through a one-call sd_ token); it is never offered in the fact-check or LaTeX-fix lane or in any chat a module runs in (MODULE_RUN_CHAT_KINDS: check, latex_fix, selection_action), so a module's run cannot start another. Browsing agents use /g/module (lib/get-ops.ts, token=<sd_ token>). /start documents both.

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:

Every check row has one shape, whatever its state (VerifierRowView): a mark, the check's label, one line of words, one action — the same type, spacing, truncation and hover for all of them. The rail is calm (Belinda 2026-09-30, "we don't need to do red, green"): no verdict colors. The mark (RailMark) is a plain stone dot that glows softly while the check runs, and an empty ring for a check not added.

Installed verifiers first (each check an installed module's manifest verifies, the same list the page switches on), one row each: the quiet mark, the verifier's name, and its words for the open document — the running words and a clock while it runs, else its last result in the registry's plain words (2 of 4 proved, A source disagrees · 2 of 6, 4 checked · Matches the paper, 1 of 4 · Says something different) or, before a first run, Not checked yet (Not compared yet for Matches the paper?). Matches the paper? counts the paper's statements: only verdicts for declarations paired to a .tex statement, never every helper the agent wrote (auditRailRow). Its ⋮ shows on hover. Clicking a row takes you to the document the check is checking or last checked (the row's openDocument, never the chat): that file, or when it is already open, its results — the claim cards (the first one selected), the Lean or Graph view beside the paper. The page remembers each check's document as the file its run started on, else the open file once it holds the check's answer (claim cards, a verdict, a paper with its .lean); while a check runs its click goes to the run's file, never merely the open one (checkDocumentTarget in lib/workspace/check-document.ts). A renamed or deleted file is forgotten: after a reload, or then, the LaTeX checks go to the paper with a .lean beside it, else the first .tex. A row that says Try again · … (about the open paper) tries again on click. Its ⋮ holds Model · <name> (the picker, see "What each module runs on" below) and Remove. The built-ins (Fix my LaTeX, AI-written?) take no row: nothing to add or remove. When two or more checks cannot help with the open file (activeVerifiers: its extension is not in their documents, or nothing is open), they fold into one line of the same shape saying what they are for ("2 mods · For LaTeX and Lean files", sidebar-checks-away), that glows while any check it holds runs, whose Show opens them.
Other installed modules, each with what it does for you, muted after its name (moduleWords: a paper template "Sunny follows its rules"). A check module has no row of its own: its checks are its rows, and the skills it brings (seeded, or named by its instructions, like lean4) are theirs, not rows either.
Checks you could add: 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), then the picks that switch on a check not on yet (their verifies; a pick whose checks are all on is not offered), each an empty ring, its pitch and Add, always showing. Two verifiers can share a module — Lean and the audit both come with lean-blueprint — so there is one row per module.
Browse the gallery, where verifiers lead as "Checks your work" and carry the Verifier kind. The header's + Add menu leads with them too: each check by its label over its pitch.

Add runs the connect route for VerifierSpec.module: files seed at the root, instructions append, the row moves up saying Not checked yet, and the header cluster gains its chip. The first run's answer becomes its words. Remove asks first, by the names the rail shows ("Remove Check with Lean and Matches the paper?", never the module's catalog name), and says what goes: their marks and buttons; your files, comments and chats 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).

What each module runs on

Every module says what does its work, and a module whose work is an agent run lets the workspace pick its model (Belinda: "the model should be choosable in the modules… but it should still look all simple").

The registry declares it. runsOn: { model } for a module run by an agent turn (Is it true?, Check with Lean, Matches the paper?, and Fix my LaTeX's fixes), with the model the app's own start of it passes (the fix chat, the formalization and audit chats; null: a new chat's model, which is the workspace default); runsOn: { engine } for a fixed checker (AI-written? is Pangram). madeBy is the verb its one quiet line starts with. A module's own default is its manifest: the model of an action with a verifier comes before the registry's (moduleModelFor(id, picked, defaults)), so the rail names what that action runs on.
The pick is per workspace per module: projects.module_models ({ "<verifier id>": "<gateway model id>" }, migration 20260930120000_projects_module_models.sql), because a built-in (Fix my LaTeX) has no install row. GET /api/workspace/modules returns the picks as models, each manifest action's pinned model as defaults ({ <verifier>: <model> }) and a new chat's model as defaultModel; PATCH /api/workspace/modules { projectId, module, model | null } sets one in a single statement (set_module_model, so two editors picking at once both keep theirs; owners and editors; a module with an engine refuses; the model must be in the gateway catalog, normalizeSupportedModelRef). null goes back to the default, and for compile moves the one fix chat off the old pick (unpinLatexFixChat; a model chosen in the chat itself stays). A read that fails is no pick (readModuleModels in lib/workspace/module-models.ts), so code shipped before the migration lands runs on the defaults.
Every start reads it, so runs Sunny or an outside agent starts obey it too: moduleRunModel (pick, else the manifest action's model, else the registry default) behind createWorkspaceChat({ module }) — the invoke route passes the action's verifier, POST /api/workspace/chats takes module (the LaTeX fix chat sends compile, startFormalizationRun and friends lean, startFaithfulnessAudit audit) — the campaign's dispatchRun (lean, or audit for the audit leg), and the claim-split pre-flight's BYOK waiver (claim). The one fix chat is reused forever, so ensureLatexFixChat({ model }) moves it to the pick before the fix is sent.
Picking. An added check's rail row has a ⋮ (ModuleRowMenu) with one line, Model · GPT 6 Astra, that opens the composer's own model list (ModelPickerList, components/workspace/model-picker-list.tsx — the chat composer renders the same component), and Remove. Fix my LaTeX has no rail row, so its line lives in the compile status popover ("Fixes by GPT 6 Astra", compile-status-model), opening the same list inline (ModuleModelChooser). A picked module's list starts with Default · <name> (module-model-default), which saves null. Readers see the line, not the picker. A signed-out visitor's free runs are all pinned to ANON_RUN_MODEL_ID (the server rewrites chats.model on send), so every seat names that model (useWorkspaceVerifiers(projectId, pinnedModel), ModulesSection pinnedModel) and offers no picker, with the composer's note: "Free runs use GPT 6 Astra. Sign in to pick other models." (module-model-pin-note).
Saying it. One quiet line, in the registry's words (madeByWords, the catalog display name via formatModelLabel): the claim card says "Checked with GPT 6 Astra · 3 credits" (claim-verification-made-by; the comments route fills thread.madeBy for one file's threads, never the workspace-wide list, from the run chat's credit_events usage rows: the model that ran and the micros of the run's first turn only, so an @sunny follow-up is not counted — withMadeBy, indexed by credit_events_chat_usage); a check's start notice says "Runs on …" (runsOnWords, the pick) and its finish notice the made-by line with the model its run chat actually ran on (the claim cards' ledger model, the formalization or audit chat's chats.model; workspace-notice-made-by); the rail row's hover names the model.
Engines name their real version, parsed from their own answers, never a constant here (lib/workspace/engine-versions.ts): the compile popover says "Built with pdflatex · TeX Live 2025" from the TeX log's banner (texEngineWords); the Lean chip's list ends "Checked by Lean 4.34.1 · Mathlib v4.34.1" from the pool's versions (leanEngineWords; sandbox/lean_pool.py _engine_versions(engine) reads what that check ran on: the CLI lane's /opt/mathlib/lean-toolchain and /opt/mathlib-version.txt, the REPL lane's /opt/repl/lean-toolchain and no Mathlib; the pool needs a Modal redeploy via scripts/redeploy.py before versions arrives); the AI-written? card says "Checked by Pangram 3.0" from the task's version (pangramEngineWords).

5. Status colors

status	color	glyph
`ok`	green	filled
`conditional`	green	hollow ring
`warn`	orange (orange-600, never amber)	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. On a one-line surface the color lives only in the dot and the words stay stone; on a card or popup it lives in the verdict words. The Modules rail shows no status color at all (§4).

6. Adding a verifier

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, its speed, Sunny's offer and its cost (the before-you-start line reads them), recommend — which workspace files call for it —, which files it applies to once on (documents), and whether the text bubble offers it on a selection (onSelection, narrowed by selectionDocuments).
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); model is the action's other knob. The invoke route reads those — never an identity.
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.
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).
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.
If it needs a full view, register a companion leaf in the view registry (registerView, TexCompanionMode) — see the Workspace SDK §12.
If a failing verdict has a repair, offer the agent hand-off from the evidence, never from the status alone.
Give the rail its status and summary: verifierRows in page.tsx maps the verifier's id to { status, summary, onOpen, openDocument } from its pipeline (onOpen the evidence, openDocument the rail's click).
Add its row to §2 above and a test in tests/ui/verifiers.test.ts; the doc test fails until the row exists.
Give it a starter in MODULE_STARTERS (§3, "Starting a run without a click") and add its id to run_module's list and /start; tests/api/module-run.test.ts fails until all three agree.

7. Tests

Verifier	Unit	API	Smoke
`compile`	`tests/ui/use-latex-compile-.test.ts`, `use-latex-fix-flow.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
`stale`	`tests/ui/stale-check.test.ts` (registry, verdict words, cards, rows, folder index), `agent-ts/tests/stale-check-lane.test.ts` (trigger, tools, guard, prompt, card line), `thread-fallback.test.ts`, `claude-task-subagents.test.ts`	`tests/api/assistant-action-invoke-route.test.ts` (folder check), `claim-split-route.test.ts`, `checks-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; the before-you-start line for every budget)
this page	`tests/ui/verification-doc.test.ts` (every verifier, verdict and status; the identifiers, keys and kinds §8–§11 name)
a run without a click	`agent-ts/tests/run-module.test.ts` (the tool, its lanes)	`tests/api/module-run.test.ts` (each module's start, each refusal, the route caller, the drift guard), `tests/api/get-ops.test.ts` (`/g/module`)
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`
Gate	`activeVerifiers` (built in, `.tex`) + `canCreateWorkspacePath(root)`	`activeVerifiers` (`enabled.has('lean')`, `.tex` / `.lean`) → `leanCheckProjectId`	the installed action with `verifier: 'claim'`; owner/editor with write
Units it detects	the root `.tex` (`resolveLatexRoot`)	statements: `listFormalizableStatements` (what the PDF shows: `%` comments, `\iffalse … \fi` and verbatim / comment blocks are skipped, a `%` in `\url` / `\href` / `\verb` is text, a theorem's `\item[(a)]` parts are the theorem while a free-standing `\item[(i)]` with math is a statement of its own, names follow the PDF's numbering), 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 wash 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; the fact-check lane on its triggering turn (`factCheckLaneSystemPrompt`, web tools only)
Model	the workspace's pick for `compile` (`module_models`), else `LATEX_FIX_CHAT_MODEL` for the fix chat	the pick for `lean` / `audit`, else `FORMALIZATION_MODEL` (`openai/gpt-6-astra`, the registry default) for the run chat and the manifest action's `model` for the selection action	the pick for `claim`, else the manifest action's `model`, else the workspace default
Onboarding	SyncTeX tip card	none	none
Persisted prefs	`sundial:latex-autocompile`, `sundial:latex-scroll-sync`, `sundial:synctex-tip-seen`, `sundial:show-latex-format-bar`, `sundial:latex-workbench-editor-fraction`	none	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; 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 Lean's and the compile's, never a claim's), ClaimVerificationThreadCard in every editor's lane (markdown and .tex), the PDF's check tint (no pin; narrowed to the quote's own words when the page's text layer shows them, else its SyncTeX lines; a click on it selects the card, a link or pin over it keeps its own click; a double-click ties the check under the pointer, and the tie itself never selects a card, so a double-clicked word never reopens a lane closed on purpose) 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 page shows it by the paper: a refutation says "It's false" on Check with Lean's surfaces while sourceHashes.tex matches the saved .tex (useAuditVerdicts' current); a counterexample is about the paper's statement, so later edits to the .lean don't hide it. 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-fix-flow.ts (Fix my LaTeX), use-latex-autocompile.ts, use-latex-fix-resume.ts, lib/latex/{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,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, selectionChecks, 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, beforeYouStart), lib/workspace/verifier-budget.ts (VerifierBudgetContext), lib/credits/constants.ts (the costs a check quotes), components/workspace/use-workspace-verifiers.ts (useWorkspaceVerifiers: enablement from the installed modules), lib/workspace/gutter-glyphs.ts (mergeGutterGlyphs), latex-monaco-markers.ts (installGutterGlyphs), collab-code-editor.tsx (the merge, the claim wash from thread anchors, the chip mount, the bubble). The live step line: agent-ts/src/session/step-stamp.ts (createStepReader, createStepStamper), lib/workspace/{sunny-steps,chat-steps}.ts, liveFromMessageEvent in workspace-chat-runtime-effects.ts, components/workspace/{elapsed.tsx,use-sunny-reaction.ts}.

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:

Two auto-compile engines (browser and brain), handshaking through holdAutoCompile / markBackgroundCompiled alone.
Three result sinks, three readers (files, threads, chat messages); the gutter is the only meeting point, through three adapters in collab-code-editor.tsx.
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

// 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.