At this seminar I'll give a practice talk for my presentation at TyDe next month. 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. Pipit is 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 which is suitable for compilation and real-time execution on embedded devices. In this talk I'll describe a small case study of a driver for an accelerometer which communicates over the I2C bus, and show how we can reuse F*'s tactics for both proving properties and generating executable code.