An abstract domain of convex polyhedra, formally verified in Coq for formally verified static analyzers, such as Verasco.
PADEC is a framework to build certified proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions.
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.