Scade is a well-known commercial tool widely used in the development of safety-critical embedded control software, whose modeling language is a synchronous language extended from Lustre, a synchronous data-flow language. Correct compilation of synchronous languages, including Lustre, has attracted much attention in recent years, and has been addressed in many studies through formal verification. To build a formally verified compiler for such a language, it is a common practice to compile the source program into a C-like program first, and then to compile it into low-level machine-dependent code using a formally verified backend compiler such as the CompCert compiler, where the correct compilation of temporal operators is crucial. In this study, the formally verified compilation of Scade-like temporal operators is introduced, which is used in a formally verified compiler projects, where a Lustre-extended synchronous language is translated into the front-end intermediate language Clight in the CompCert compiler. The compilation and formal verification of temporal operators are divided into two key stages, which are implemented in the interactive proof assistant Coq.