The Coq Proof Assistant

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.