Verified Display for Language Interfaces to Optimisation-Based Control

Language interfaces can answer questions about recorded runs of optimisation-based controllers. Verifying the structured claims a language model proposes does not ensure that its final prose contains only those claims. Across six models, answers whose claims passed verification still carry a scorer-flagged addition in 21 to 28 percent of paired cases. We introduce a verified display layer. The model proposes typed claims, deterministic checks evaluate them against the recorded solve, and a closed renderer turns only accepted claims into text that decodes back to those claims. In a paired experiment that changes only the displayed text, rendering removes every scorer-flagged addition and introduces no reverse transition; the preregistered split reproduces this result. Human adjudication finds a smaller but persistent rate of false statements in model-written prose. With tool calling, the layer trades coverage for lower displayed risk: useful coverage rises in dispatch and falls in HVAC, and the confidence interval of the pooled change includes zero. The guarantee covers declared predicates over the recorded committed solve, rather than controller correctness, plant behaviour, or causal explanation.