The Rocq Prover is an interactive theorem prover, or proof assistant. This means that it is designed to develop mathematical proofs, and especially to write formal specifications: programs and proofs that programs comply to their specifications. An interesting additional feature of Rocq is that it can automatically extract executable programs from specifications, as either OCaml or Haskell source code.
Last modified 17 February 2026