Robinson, AmosPotanin, Alex2025-05-232025-05-2397839597734161868-8969ORCID:/0000-0002-4242-2725/work/184102656dblp:conf/ecoop/RobinsonP24WOS:001533999700034http://www.scopus.com/inward/record.url?scp=85205028976&partnerID=8YFLogxKhttps://hdl.handle.net/1885/733751699Synchronous 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 synchronous 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 executable code in a subset of F✶ which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program.28enPublisher Copyright: © Amos Robinson and Alex Potanin;Lustrereactivestreamingverification202410.4230/LIPIcs.ECOOP.2024.3485205028976