Verified Confinement: A Case-Study Pattern for Confining LLM Output Behind Deterministic Verifiers

LLM code assistants and LLM-integrated systems more broadly are difficult to trust because nothing in their construction stops a hallucinated answer from being treated as a correct one. We report a case study: three real systems (a spreadsheet auditor, a government-record filing assistant, and an LLM-in-the-loop cross-language code-porting pipeline), built by one author for unrelated hackathons, that converged on the same architecture: a narrow generative surface the model is confined to, a deterministic verifier checking an artifact independent of the model's self-report, non-authoritative typing that makes unverified output structurally impossible to mistake for verified, and a defined failure/degradation mode. We call this Verified Confinement; it is close kin to test-driven automated program repair, but recurs even outside code. This is convergent design within one engineer's practice, not a general law, a limit the paper's Discussion section names directly; beyond that anecdote, we also report a fourth system built to the pattern a priori, a fixed audit checklist two separate blind agents apply to this paper's own systems with matching verdicts, and a code-level audit of nine third-party systems against that same checklist, finding a majority but not all: four full matches, three partial, and two informative negatives, one failing on breadth and one on verifier independence specifically. The fourth system, a Dafny generate/verify/repair loop, fixes 17 of 24 real bugs against a validated 29-mutation catalog, after our harness caught and fixed a real false positive of its own (an empty reply Dafny trivially "verified"). Evaluated against a live, free-tier model across all four systems: an anti-hallucination gate caught every one of three spontaneous fabrications with zero false positives across 54 trials; a grounding fence rejected a real out-of-context interpretation; confined interpretation beat a template-only baseline on 53-87% of reachable trials in a blind-judged ablation, failing safely on the rest. A separate, adversarial check, where the model drafts once and self-certifies without seeing the verifier's verdict, puts false-acceptance estimates at 33-67%, worst where verification matters most. A frontier model (Claude Sonnet 5) closes this gap entirely on proof-repair (0/24 vs. 44.4%, p=0.0004), substantially on sheet-auditor (1/15 vs. 10/15), and on sched-port's budget-blocked repairs (7/8 vs. 1/8), but not on epf-filer (6/18, 33.3%): whether it closes depends on why the gap exists, not model scale. A held-out spreadsheet corpus confirms sheet-auditor's pipeline generalizes beyond its tuning corpus (92.9% recall vs. 98.1%), and a context-free agent given only the integration code re-derives the same decomposition, correctly reporting it absent in a synthetic system built to lack it. We also report what did not work: a direct-prompt baseline, a reasoning-effort tuning tension, and a k-sample self-consistency check that closed no gap. We state plainly what this is not: no machine-checked proof, no claim of novelty. Reporting negative results alongside positive ones, precisely, is itself the contribution.