Coq

Coq is "a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs." [1]

Coq can be considered as ocaml package (actually it is), which can be installed via opam:

> opam pin add coq 8.17.1

Full guide is here.