Vélus is a formally verified compiler for the synchronous dataflow language Lustre. It includes a formal semantic model for its input language which is used in its end-to-end compilation correctness proof.

We propose automatic tooling to verify properties of Vélus programs against this semantic model. It includes generic lemmas written once and for all, and discharges the program-specific proof to SMTCoq, a plugin that calls an SMT solver with a boolean formula and rebuilds a Rocq proof term of validity of the formula. Our approach is fully verified with respect to the reference semantic model.