An abstract domain of convex polyhedra, formally verified in Coq for formally verified static analyzers, such as Verasco.
An OCaml wrapper certified in Coq to check answers of 2018 state-of-the-art SAT-solvers.
A Coq library to embed untrusted imperative OCaml computations (through Coq extraction toward OCaml)
A version of the CompCert certified compiler with instruction scheduling for pipelined processors and in particular for Kalray VLIW core (with explicit instruction parallelism at the assembly level).
A tactic for simplifying linear arithmetic within Coq goals, with oracles from the VPL library.