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