Welcome!
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.
The Reference Manual and the Standard Library documentation are the primary documentation for Coq. However, to learn about Coq, we recommend starting with a tutorial or book, such as those listed on the documentation page.
You don't need to install Coq to get started: you can run Coq in your browser using jsCoq!
Eventually you'll probably want to install Coq on your system with a user interface of your choice.
Coq has a large and active user community. They contribute formal developments, Coq extensions, and tools based on Coq (see the Coq Package Index and the Awesome Coq curated list of projects and resources). We have a multi-lingual Discourse forum and a Zulip chat.
Note our code of conduct that applies to all spaces managed by the Coq team, including online forums and physical events.
Coq is free, open-source software. Its development is largely supported by Inria, a French public computer science institute, but anyone can follow and participate in the process on GitHub. The Coq Team manages the development of Coq: it is an international mix of developers and power users from academia and industry.
You can contribute to the development of Coq by reporting bugs, suggesting enhancements, submitting pull requests, improving the documentation and in many other ways.
Academic and industrial users are also encouraged to contribute financially to support the maintenance and evolution of Coq and its ecosystem through the Coq Consortium.