The users of Coq

As a generic proof assistant, Coq can be used in various ways either to write formal specifications of system and software, or as a basis tool for software verification. You can refer to our repository of users' contributions to get an overview of existing formalizations written in Coq. You can also visit the page dedicated to related tools to see a list of extensions and tools based on Coq.

You can interact with other users of Coq through the Coq-club mailing list; the list archives are also a good source of information. There is also a wiki dedicated to Coq: Cocorico!, where you can share your experience with other users.

Coq does not necessarily have to be used with the standard sets of tactics and standard library coming bundled with the system. Some users might want to use their own specialized tactics and/or libraries. Examples include the Ssreflect project, the Y-not project, Software Foundations, Lambda Tamer, Charguéraud's tactics, CompCert, ...

The Coq development team

You can contact directly the Coq developpers through the Coq-dev mailing list. If you want to report a bug, please consider using our bug tracking system. The Coq developers and interested users gather for working groups a few times a year.