The Vélus project is an ongoing and long-term effort to extend techniques for formal specification and verification in Interactive Theorem Provers to the languages, tools, and applications of Model-Based Development.

We focus specifically on dataflow synchronous languages like Lustre and Scade and we work in Coq. The main concrete result of our project is the Vélus verified Lustre compiler. This compiler can be seen as an extension of CompCert for compiling Lustre.

Model-Based Development

Embedded control software defines the interactions of specialized hardware with the physical world. It normally ticks away unnoticed inside systems like medical devices, trains, aircraft, satellites, and factories. But this software is complex and potentially serious errors are difficult to avoid, especially over many years of maintenance and reuse. Engineers have long designed such systems using block diagrams and state machines to represent the underlying mathematical models. The key idea of Model-Based Development is that such models can be executable and serve as the base for simulation, validation, and automatic code generation.

Interactive Theorem Provers

Interactive theorem provers, also sometimes called as proof assistants, are software tools for functional programming, formal specification, and machine-checked proof. Broadly speaking, our goals are to

1. Develop semantic models for the source language inside an interactive theorem prover.

2. Develop a compiler with a formal proof that the semantics of a source model are implemented by the code generated for it.

3. Provide tools for interactive reasoning about source models and libraries with results guaranteed down to the code that executes.