Rocq (formerly coq) is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using OCaml and Dune.

WWW: https://rocq-prover.org/
