This preprint proposes Truth-Aware Decoding (TAD): a program-logic, knowledge-base–aligned, decode-time guard system for LMs; it casts oracle filtering as a logic judgment, proves when greedy steps are safe under sound/complete guards, and defines an entropy-style invariant for factual risk. Case studies report fewer hallucinations without hurting throughput, with Lean-verified artifacts.
