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.

The stable version of Coq is version 8.2. Released in February 2009, it brings Haskell-style type classes, various evolutions of the arithmetic libraries, and many other various improvements and extensions regarding the module system, tactics, syntax, etc. (see the more detailed description and the summary of changes). Note that a few evolutions of Coq may require adaptations for upgrading from Coq 8.1.

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 (see Coq Users' Contributions), extensions of Coq, and tools based on Coq (see Related Tools).