This paper proves that complete formal verification of real software systems is structurally impossible — not as a practical limitation of current tools, but as a mathematical consequence of what formal languages can and cannot express. The core result (the Verification Regress Theorem) establishes that for any formal verification of any real system, the claim that the verified proposition correctly describes the system cannot be established within the formal language or within any finite tower of metalanguages. The proof applies Tarski's undefinability theorem iteratively: formalizing the correspondence between a proposition and the system it describes requires a richer metalanguage, which generates a new correspondence claim that requires a still richer metalanguage, producing an infinite regress that no finite extension of the formal framework can resolve. The result does not argue against formal verification. It argues for precision about what the word "verified" means. Formal verification establishes that a proof is valid relative to a proposition. Whether the proposition describes the real system is a correspondence judgment that lies outside the formal apparatus and cannot be brought inside it. This judgment is sound when made by competent engineers with domain expertise. It is unsound — or absent entirely — when AI systems generate specifications, code, and proofs without human engagement with the underlying problem. The paper discusses five caveats to prevent misapplication of the result: (1) the theorem concerns formal verification, not human knowledge; (2) it does not invalidate formal verification; (3) partial closure of specific correspondence gaps is possible and valuable (as demonstrated by projects like seL4, CompCert, and Dafny); (4) the strength of the unverified correspondence assumption varies by tool and methodology; and (5) the functionalist objection — that intentionality reduces to computation — does not escape the regress. Implications are drawn for the verification of AI-generated software artifacts, including spec-driven development frameworks (Kiro, Spec Kit, Tessl, OpenSpec), LLM evaluation, and AI governance. The paper introduces the concept of "intent evaporation" — the systematic conversion of human purpose into measurable proxies treated as lossless — and connects the result to recent work on "ersatz meaning" (Hattiangadi & Schoubye, 2025) and "intent debt" (Storey et al., 2026). A companion article discussing the practical implications of this result for engineers and technical leaders is published on Medium. Subjects/disciplines: Computer Science, Software Engineering, Logic in Computer Science, Philosophy of Computer Science