The formal verification and AI safety literature frequently cite total languages as a solution to the halting problem. This paper argues that this claim relies

The formal verification and AI safety literature frequently cite total languages as a solution to the halting problem. This paper argues that this claim relies on a binary reduction of a trinary problem. While total languages provide an exit proof (halting), they cannot provide a correct-exit proof without step-by-step verification, which is itself the halting problem. Using Rice’s Theorem (1953) and Turing’s second proof (1936), I demonstrate that "early termination"—halting at an unintended point with incorrect output—is a non-trivial semantic property and therefore undecidable. The safety guarantees currently being marketed are often just tautologies where "termination" has been swapped for "safety". No novel math here—just a careful reading of the foundational proofs we’ve had for decades.