Coq

Awesome Coq Awesome

A curated list of awesome Coq libraries, plugins, tools, and resources.

The Coq proof assistant provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs.

Contributions welcome! Read the contribution guidelines first.


Projects

Frameworks

  • CoqEAL - Framework to ease change of data representations in proofs.
  • Fiat - Mostly automated synthesis of correct-by-construction programs.
  • FreeSpec - Framework for modularly verifying programs with effects and effect handlers.
  • Iris - Higher-order concurrent separation logic framework.
  • Q*cert - Platform for implementing and verifying query compilers.
  • Verdi - Framework for formally verifying distributed systems implementations.
  • VST - Toolchain for verifying C code inside Coq in a higher-order concurrent, impredicative separation logic that is sound w.r.t. the Clight language of the CompCert compiler.

User Interfaces

  • CoqIDE - Standalone graphical tool for interacting with Coq.
  • Coqtail - Interface for Coq based on the Vim text editor.
  • Proof General - Generic interface for proof assistants based on the extensible, customizable text editor Emacs.
  • Company-Coq - IDE extensions for Proof General's Coq mode.
  • jsCoq - Port of Coq to JavaScript, which enables running Coq projects in a browser.
  • Jupyter kernel for Coq - Coq support for the Jupyter Notebook web environment.
  • VSCoq - Visual Studio Code extension.

Libraries

  • ALEA - Library for reasoning on randomized algorithms.
  • Bignums - Library of arbitrary large numbers.
  • CoLoR - Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library.
  • coq-haskell - Library smoothing the transition to Coq for Haskell users.
  • Coq-std++ - Extended alternative standard library for Coq.
  • ExtLib - Collection of theories and plugins that may be useful in other Coq developments.
  • FCSL-PCM - Formalization of partial commutative monoids as used in verification of pointer-manipulating programs.
  • Flocq - Formalization of floating-point computations.
  • Formalised undecidable problems in Coq - Library of undecidable problems and reductions between them.
  • Hahn - Library for reasoning on lists and binary relations.
  • Metalib - Library for programming language metatheory using locally nameless variable binding representations.
  • Paco - Library for parameterized coinduction.
  • Relation Algebra - Modular formalization of algebras with heterogeneous binary relations as models.
  • TLC - Non-constructive alternative to Coq's standard library.

Package Management

  • coq_makefile - Build tool distributed by Coq and based on generating a makefile.
  • Coq Package Index - OPAM-based collection of Coq packages.
  • Docker-Coq - Docker images for many versions of Coq.
  • dune - Composable and opinionated build system for Coq and OCaml (former jbuilder).
  • Nix - Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks.
  • Nix Coq packages - Collection of Coq-related packages for Nix.
  • OPAM - Flexible and Git-friendly package manager for OCaml with multiple compiler support.

Plugins

  • AAC Tactics - Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.
  • Coq-Elpi - Plugin for the Embeddable Lambda Prolog Interpreter.
  • CoqHammer - General-purpose automated reasoning hammer tool that combines learning from previous proofs with the translation of problems to automated provers and the reconstruction of found proofs.
  • Equations - Function definition package for Coq.
  • Gappa - Tactic for discharging goals about floating-point arithmetic and round-off errors.
  • MetaCoq - Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins.
  • Mtac2 - Plugin adding typed tactics for backward reasoning.
  • Paramcoq - Plugin to generate parametricity translations of Coq terms.
  • QuickChick - Plugin for randomized property-based testing.
  • SMTCoq - Tool that checks proof witnesses coming from external SAT and SMT solvers.
  • Unicoq - Plugin that replaces the existing unification algorithm with an enhanced one.

Tools

  • CFML - Tool for proving properties of OCaml programs in separation logic.
  • CoqOfOCaml - Tool for generating idiomatic Coq from OCaml code.
  • coq-dpdgraph - Tool for building dependency graphs between Coq objects.
  • coq-tools - Scripts to help construct small reproducing examples of bugs, remove unneeded imports, etc.
  • Cosette - Automated solver for reasoning about SQL query equivalences.
  • hs-to-coq - Converter from Haskell code to equivalent Coq code.
  • lngen - Tool for generating locally nameless Coq definitions and proofs.
  • Menhir - Parser generator that can output Coq code for verified parsers.
  • mCoq - Mutation analysis tool for Coq projects.
  • Ott - Tool for writing definitions of programming languages and calculi that can be translated to Coq.
  • SerAPI - Library and tools for (de)serialization of Coq code to and from JSON and S-expressions.

Type Theory and Mathematics

  • Analysis - Library for classical real analysis compatible with Mathematical Components.
  • Category Theory in Coq - Axiom-free formalization of category theory.
  • CoRN - Library of constructive real analysis and algebra.
  • Coquelicot - Formalization of classical real analysis compatible with the standard library and focusing on usability.
  • Four Color Theorem - Formal proof of the Four Color Theorem, a landmark result of graph theory.
  • GeoCoq - Formalization of geometry based on Tarski's axiom system.
  • Homotopy Type Theory - Development of homotopy-theoretic ideas.
  • Mathematical Components - Formalization of mathematical theories, focusing in particular on group theory.
  • Math Classes - Abstract interfaces for mathematical structures based on type classes.
  • Odd Order Theorem - Formal proof of the Odd Order Theorem, a landmark result of finite group theory.
  • UniMath - Library which aims to formalize a substantial body of mathematics using the univalent point of view.

Verified Software

  • CompCert - High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.
  • Fiat-Crypto - Cryptographic primitive code generation.
  • JSCert - Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter.
  • lambda-rust - Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries.
  • Verdi Raft - Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.

Resources

Community

Blogs

Books

  • Coq'Art - The first book dedicated to Coq.
  • Software Foundations - Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners.
  • Certified Programming with Dependent Types - Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
  • Program Logics for Certified Compilers - Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.
  • Formal Reasoning About Programs - Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
  • Programs and Proofs - Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
  • Computer Arithmetic and Formal Proofs - Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.
  • The Mathematical Components book - Book oriented towards mathematically inclined users, focusing on the the Mathematical Components library and the SSReflect proof language.

Tutorials and Hints