← All repos

rocq

The Rocq Prover is an interactive theorem prover, or proof assistant. 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.

GitHubrocq-prover.org
coqdependent-typesproof-assistanttheorem-proving
Browse cluster: Lean4 Formal Verification & Cryptography →
48,743commits
363contributors
18languages

Tech stack & purpose

The Rocq Prover is an interactive theorem prover and proof assistant that provides a formal language for writing mathematical definitions, executable algorithms, and theorems alongside a semi-interactive environment for developing machine-checked proofs. Built in OCaml, the project supports dependent types and proof automation, and is developed as an open-source effort with extensive continuous integration infrastructure across Docker, Nix, and benchmarking systems. The repository includes comprehensive developer documentation covering topics like the proof engine, plugin development, parsing, and debugging, along with tooling for managing external library compatibility testing through overlay mechanisms.

Community & reference links

Languages

OCaml
73.5%
Rocq Prover
22.6%
Shell
1.3%
TeX
1.2%
C
0.6%
Makefile
0.2%
Python
0.2%
Nix
0.1%
Emacs Lisp
0.1%
V
0.0%
CSS
0.0%
Dockerfile
0.0%
Dune
0.0%
HTML
0.0%
JavaScript
0.0%
Batchfile
0.0%
Verilog
0.0%
sed
0.0%

Contributors (top 30 of 363)