Several tools are being built on top of Coq, for software verification purposes.

• Why is a verification conditions generator back-end.
• Krakatoa is a Java code certification tool that uses both Coq and Why to verify the soundness of implementations with regards to the specifications.
• Caduceus is a verification tool for C programs, built on top of Why.
• Concoqtion is a dependently-typed extension of Objective Caml (and of MetaOCaml) with specifications expressed and proved in Coq.
• Ynot is an extension of Coq providing a "Hoare Type Theory" for specifying higher-order, imperative and concurrent programs.
• Ott is a tool to translate the descriptions of the syntax and semantics of programming languages to the syntax of Coq, or of other provers.

• LNgen is a tool for generating Coq code for the infrastructure associated with a locally nameless representation;
• Hybrid is a package for reasoning with Higher Order Abstract Syntax;
• GMeta is a generic formal metatheory framework for various first-order representations;
• Rainbow automatically generates Coq proofs from termination certificates.

Coq can be used in text mode or in graphical mode using its gtk-based integrated development interface CoqIde. Alternative third-party graphical interfaces are also available :

• The Proof General Emacs/XEmacs interface by David Aspinall with Coq support by Pierre Courtieu;
• a syntax highlighting script and an indentation script for Vim by Vincent Aravantinos;
• the ProofWeb online web interface for Coq (and other proof assistants), with a focus on teaching;
• ProverEditor is an experimental Eclipse plugin with support for Coq;
• for versions of Coq in old syntax (version 7.4 of 2003 and before), Pcoq is a graphical interface and TmCoq is an integration of Coq with TexMacs.

• The Hypertextual Electronic library of Mathematics (HELM), located at Bologna University (a component of the MoWGli project);
• coq-graphs is a graphical tool to visualize dependencies and coercion graphs in Coq documents.