ABSTRACT. We present a formalization of a translation from LTL formulae to generalized Büchi Automata in the HOL4 theorem prover. Translations from temporal logics to automata are at the core of model checking algorithms based on automata-theoretic techniques. The translation we verify proceeds in two steps: it produces Very Weak Alternating Automata at an intermediate stage, and then ultimately produces a generalized Büchi Automaton. After verifying both transformations, we also encode both of these automata models using a generic, functional graph type, and use the CakeML compiler to generate fully verified machine code implementing the translation.