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.
- Jessie is a verification tool for C programs (plugin of the Frama-C framework).
- 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.
- Autosubst is a tool for automatizing the infrastructure and proofs associated with a De-Bruijn-index representation of binders;
- LNgen is a tool for generating Coq code for the infrastructure and proofs 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;
- The Coqoon Eclipse plugin for Coq development (based on Wenzel's asynchronous PIDE framework);
- The Coq PIDE Jedit (proof of concept) plugin for Coq development (also based on asynchronous PIDE framework);
- 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;
- the PeaCoq online web interface for Coq (by Valentin Robert);
- ProverEditor is an experimental Eclipse plugin with support for Coq;
- other information possibly available on the Cocorico wiki.
- coq-graphs is a graphical tool to visualize dependencies and coercion graphs in Coq documents;
- Proviola is a coqdoc-compatible documentation tool for showing how proof states evolve as one goes along a proof script;
- The Hypertextual Electronic library of Mathematics (HELM) was a component of the MoWGLI project for searching and browsing libraries. It is unmaintained.