Current research
Collaboration with NASA: Enhancing FRET with NASA
As part of our ongoing collaboration with NASA, we are revisiting the FRET (Formal Requirements Elicitation Tool) project, an interactive platform that translates structured natural language requirements into formal specifications expressed in temporal logic. With the support of an expert in pure and applied logic, we aim to reimagine FRET with a focus on enhanced logical simplicity without compromising computational efficiency, tailored to technically proficient users. Our objective is to extend FRET through our PCSS methodology, ultimately integrating it into the Rocq proof assistant.
This enhanced version would enable:
  • Formal verification of correctness: proving the semantic equivalence between the natural language requirements and their formal logical representation.
  • Certified code extraction: generating executable code in OCaml, Haskell or C from verified specifications, with varying degrees of formal guarantees depending on the target language.
By bridging requirements engineering with proof-based verification and trustworthy code generation, this initiative brings FRET closer to a verifiable-by-construction tool chain for mission-critical systems development.

Advancing Low-Level Software Verification for Embedded Systems
This project focuses on developing verified software for embedded devices using the Rocq proof assistant, targeting platforms such as Arduino and similar microcontroller-based systems. By writing embedded code directly within Rocq and leveraging its formal verification capabilities, we can establish the correctness of system behavior. The verified code is then compiled to C using CertiCoq, a certified compiler from Coq to C, ensuring that verified properties are preserved throughout the compilation process and maintained on the hardware.
By introducing formal methods into the domain of embedded systems, this work lays a strong foundation for building reliable, mathematically verified software in safety-critical areas such as robotics, the Internet of Things (IoT), and automotive applications.

Solving Weekly rest problem with PCSS method
EU Regulation 561/2006 opens a challenge on the computation of weekly rests for drivers. While the definition on paper is very simple, it opens a complex computational problem because of the multiple choice and branching in the assignment of rests and compensations to weeks.
While developing an efficient program for that is already hard, it becomes a challenge when formal verification is also involved. We are working on reductions of the problem to other known problems, as well as developing an algorithm using backtracking and pruning over the graph of choices.
To do so, the need for a general graph library in Rocq arose. We are working on a verified library for representing polymorphic graphs and executing known algorithms over them, like DFS and BFS among others.