Please find below some selected formal developments using Rocq and the Mathematical Component Libraries:
- W-Calculus, verified semantics for a DSP-oriented synchronous programming language
- mech.v, a formalization project for mechanism design
- VerDILog, an incremental Datalog engine with support for regular queries
- ssrbit, a library for Bit Sequences and Bit Sets
- C-DFT, a constructive formalization of the Discrete Fourier Transform and some associated properties