Reactive languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small reactive language embedded in F★, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F★’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate imperative code in a subset of F★ which is suitable for compilation and real-time execution on embedded devices. This translation to imperative code preserves types by construction; the proof that the imperative code preserves semantics is ongoing.