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 formalization of programming languages semantics (e.g. the CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching.

The stable version of Coq is version 8.3. Released in October 2010, it comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. It also includes a new tactic and a few new libraries.

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