Welcome! | The Coq Proof Assistant
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 theore
You can download the current stable version, Coq 8.9.0 , released in January 2019. It features many quality-of-life improvements, including goal differences as well as numeral and custom notations.
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!
Welcome! | The Coq Proof Assistant