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. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.

You can download the current stable version, Coq 8.13.0, released in January 2021.

To use Coq, you will need a user interface. Many editor support extensions are available (for Emacs, Vim, VSCode, etc.), as well as CoqIDE, a standalone IDE for Coq. The User interfaces page provides a full list, with more details. If you are only looking for a quick way to try Coq without installing anything, we recommend you use jsCoq.

You can contribute to the development of Coq by reporting bugs, submitting pull requests, improving the documentation, and in many other ways. We are also looking for sponsors who want to contribute financially through the Coq Consortium. If you are interested, please get in touch!

The reference documentation for Coq are the Reference Manual and the documentation of the Standard Library. Other useful documents (tutorials, faq, ...) are available from the documentation page.

There is a strong and active community of users working with Coq. They are contributing formal developments, extensions of Coq (see Coq Package Index), and tools based on Coq (see Related Tools). We have a (multi-lingual) Discourse forum and a Zulip chat.