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 version of the CompCert certified compiler with added optimizations and a backend for the Kalray KVX processor.
A Coq library to embed untrusted imperative OCaml computations (through Coq extraction toward OCaml)
A tactic for simplifying linear arithmetic within Coq goals, with oracles from the VPL library.