We prove that for any formal verification of any real system, the correspondence between the formal proposition and the system it describescannot be established within any finite tower of formal languages. The proof follows from Tarski’s undefinability theorem applied iteratively: verifying that a proposition correctly describes a system requires ex-pressing a correspondence claim that, by Tarski’s theorem, cannot be formulated within the proposition’s own language. Expressing the correspondence in a richer metalanguage generates a new correspondence claim that cannot be formulated in the metalanguage, producing an infinite regress that no finite extension of the formal framework can resolve. The result is structural, not contingent on current tooling or the complexity of the target system. We discuss five caveats—concerning human knowledge, the value of formal verification, partial gap closure, varying assumption strength, and the functionalist objection—and draw implications for the verification of AI-generated software artifacts.