The synchronous dataflow language Lustre is commonly used in the development of safety-critical systems. However, existing official code generators and the SCADE KCG code generator have not been formally verified, and their inner workings remain opaque to users. In recent years, translation validation methods that indirectly verify compiler correctness by proving the equivalence between source and target code have proven successful. This study proposes a trusted compilation method for the Lustre language, based on a pushdown automaton compilation approach and a semantic consistency verification method. The proposed method successfully implements a trusted compiler from Lustre to C and rigorously proves the translation process’s correctness using Isabelle.