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.

Download the pre-built packages of the latest release for Windows and macOS; read the help page on how to install Coq with OPAM; or refer to the INSTALL file for the procedure to install from source.

The sources of the documentation can be found in directory doc. See doc/README.md to learn more about the documentation, in particular how to build it. The documentation of the last released version is available on the Coq web site at coq.inria.fr/documentation. See also Cocorico (the Coq wiki), and the Coq FAQ, for additional user-contributed documentation.

There is a file named CHANGES.md that explains the differences and the incompatibilities since last versions. If you upgrade Coq, please read it carefully.

We have a number of channels to reach the user community and the development team:

• Our Discourse forum.
• Our mailing list, the Coq-Club.
• Our Gitter channel, which is a good way to reach developers for quick chat and development questions.

See also coq.inria.fr/community.

Please report any bug / feature request in our issue tracker.

To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (coqtop -v), the configuration used, and include a complete source example leading to the bug.

Guidelines for contributing to Coq in various ways are listed in the contributor's guide.

Information about the next release is at https://github.com/coq/coq/wiki/Release-Plan

Help the Coq community grow and prosper by becoming a sponsor! The Coq Consortium can establish sponsorship contracts or receive donations. If you want to take an active role in shaping Coq's future, you can also become a Consortium member. If you are interested, please get in touch!