Natural Language Has No Formal Semantics. Verify the Decision Anyway.

Natural language has no semantics one can prove theorems about, which has kept formal methods away from the reliability problem of LLM decision systems. We do not fight that objection; we make the move compiler theory made when verifying compilers proved intractable — translation validation: do not verify the translator; verify each translation, and emit a per-instance witness. Correctness of a natural-language decision decomposes into a proven kernel (machine-checked in Lean 4 for every specification in a decidable fragment), a per-instance decision (Z3, falsifiers as cores), a conformally bounded lift, and a declared, hash-frozen authority. We instantiate the chain on statutory workers'-compensation decisions under a pre-registered, content-hash-frozen evaluation: 100% independent re-derivation and tamper detection, 100% kernel–solver agreement across two encodings, and capture of decisions that are wrong with perfect stability — invisible in principle to introspective diagnostics. Substituting a weak 8B lift for a deterministic one moves coverage from 92% to 15% while soundness is unchanged: lift quality buys coverage, never correctness. A second, sized corpus — 305 license-compliance records adjudicated by a recorded expert authority — measures the governance ladder whole and paired: 78.4% ungoverned on raw accounts, ~90% once domain-modeled (rendering-inert), 96.7% verified — exactly the Σ-determined ceiling (McNemar exact p=0.0009). One pre-registered prediction was falsified, and the falsification was then proved: the predicted outcome is unreachable under the frozen specification. Verification, we argue, should attach to decisions rather than models: stability does not transfer across models, but a certificate carried by the decision re-derives anywhere.