Related Tools

Software Verification

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.
Representation of binders and termination proofs
  • 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.
Graphical User Interfaces

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 :

Browsing, Searching and Documentation Tools
  • 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.