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, or the Bedrock verified low-level programming library), 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.6.1, released in July 2017. It features among other things a faster universe checker, asynchronous error processing, Ltac and proof search improvements, generalized intro patterns, a new warning system, patterns in abstractions, a new subterm selection algorithm, and an Ltac profiler!

The upcoming version, Coq 8.7+beta1, released in September 2017, is also available for testing. Try out its improved performances, new tactics, cumulative inductive type support, its redesigned coq_makefile and use SSReflect without having to install any external library.

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).