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.