Synchronous data-flow languages (SDFL), such as Lustre , is a concurrent language that has been widely used in safety-critical systems. Verified compilers for such languages are crucial in generating trustworthy object code. A good approach is to first translate a concurrent SDFL program to a sequential intermediate representation, such as a Clight  code, and then use an existing verified compiler such as CompCert  to produce executable object code for the target machine. A verified Sequentializer is crucial in such a verified compiler. It produces a sequential topological order among the program statements that preserve the program dependencies and the dynamic semantics of the original program. In this paper, we show such an approach for a SDFL language such as Lustre. The approach is general enough to be applicable to other SDFLs as well. It first gives a formal specification of the operational semantics, and proves its determinism property for a Lustre-like program. It then formally proves the equivalence of the original concurrent semantics and its target sequential semantics using the well-established proof assistant Coq (, ), and extracts the certified code for such a sequentializer by Coq.