This talk will present MARVeLus, a cyber-physical systems language which combines verification, simulation, and implementation. The language is based on Zélus, a modern version of Lustre, where we add refinement types and associated typing rules. Our refinement types can express temporal-logic-based safety properties and prove them using a rich type system in the style of deductive verification. The language comes with an implementation, and a platform enabling execution on physical robots. Although our current implementation is limited to verifying properties about discrete constructs of Zélus, the talk will also present early efforts extending the proof systems to continuous constructs of Zélus, inspired by differential dynamic logic.
