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.

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.