Flèche
Flèche is a new document processing engine for the Rocq Prover. Flèche is based on state-of-the-art incremental computing techniques, and has been designed from scratch to support real-time checking of hybrid and literate proof documents. Flèche is used, among others, in the following sub-projects that I also (co) maintain:
Dune Build System for Rocq
Dune is an industrial-grade build system with great features and performance. We have extended Dune to support Rocq projects, supporting most of Dune's key features such as caching and compositional builds. See Dune's Rocq Build Language Documentation for more details and a quick-start guide.
The Rocq Prover
The Rocq Prover is an award-winning interactive theorem prover based on the Calculus of Constructions. I am a member of Rocq's core team, and I help co-maintain and design several components, including Rocq's build system, the vernacular layer, and the continuous integration system.