Awesome Coq

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.

Contents

• Projects
  • Frameworks
  • User Interfaces
  • Libraries
  • Package and Build Management
  • Plugins
  • Tools
  • Type Theory and Mathematics
  • Verified Software
• Resources
  • Community
  • Blogs
  • Books
  • Course Material
  • Tutorials and Hints

Projects

Frameworks

• CoqEAL – Framework to ease change of data representations in proofs.
• FCF – Framework for proofs of cryptography.
• 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 – Extension for the Visual Studio Code editor.

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 record update – Library which provides a generic way to update Coq record fields.
• 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 – 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.
• Monae – Monadic effects and equational reasoning.
• Paco – Library for parameterized coinduction.
• Regular Language Representations – Translations between different definitions of regular languages, including regular expressions and automata.
• Relation Algebra – Modular formalization of algebras with heterogeneous binary relations as models.
• Simple IO – Input/output monad with user-definable primitive operations.
• TLC – Non-constructive alternative to Coq’s standard library.

Package and Build Management

• coq_makefile – Build tool distributed with Coq and based on generating a makefile.
• Coq Package Index – OPAM-based collection of Coq packages.
• Coq Platform – Experimental curated collection of packages to support Coq use in industry, education, and research.
• Coq-community Templates – Templates for generating configuration files for Coq projects.
• Docker-Coq – Docker images for many versions of Coq.
• Docker-MathComp – Docker images for many combinations of versions of Coq and the Mathematical Components library.
• Docker-Coq-action – GitHub container action that can be used with Docker-Coq or Docker-MathComp.
• 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.
• Hierarchy Builder – Collection of commands for declaring Coq hierarchies based on packed classes.
• Ltac2 – Experimental typed tactic language similar to Coq’s classic Ltac language.
• 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.
• coq2html – Alternative HTML documentation generator for Coq.
• 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.
• Roosterize – Tool for suggesting lemma names in Coq projects.
• 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.
• Completeness and Decidability of Modal Logic Calculi – Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL.
• CoqPrime – Library for certifying primality using Pocklington and Elliptic Curve certificates.
• CoRN – Library of constructive real analysis and algebra.
• Coqtail Math – Library of mathematical results ranging from arithmetic to real and complex analysis.
• Coquelicot – Formalization of classical real analysis compatible with the standard library and focusing on usability.
• Finmap – Extension of Mathematical Components with finite maps, sets, and multisets.
• Four Color Theorem – Formal proof of the Four Color Theorem, a landmark result of graph theory.
• Gaia – Implementation of books from Bourbaki’s Elements of Mathematics, including set theory and number theory.
• GeoCoq – Formalization of geometry based on Tarski’s axiom system.
• Graph Theory – Formalized graph theory results.
• Homotopy Type Theory – Development of homotopy-theoretic ideas.
• Infotheo – Formalization of information theory and linear error-correcting codes.
• 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.
• Puiseuxth – Proof of Puiseux’s theorem and computation of roots of polynomials of Puiseux’s series.
• 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.
• Incremental Cycles – Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.
• 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

• Official Coq website
• Official Coq manual
• Official Coq standard library
• Official Coq Discourse forum
• Official Coq Zulip chat
• Official Coq-Club mailing list
• Official Coq wiki
• Official Coq Twitter
• coq-community package maintenance project
• Coq subreddit
• Coq tag on Stack Overflow
• Coq tag on Theoretical Computer Science Stack Exchange
• Mathematical Components wiki
• Planet Coq link aggregator

Blogs

• Coq Exchange: ideas and experiment reports about Coq
• Gagallium
• Gregory Malecha’s blog
• Guillaume Claret’s Coq blog
• Joachim Breitner’s blog posts on Coq
• MIT PLV blog posts on Coq
• PLClub Blog
• Poleiro: a Coq blog by Arthur Azevedo de Amorim
• Ralf Jung’s blog posts on Coq
• Thomas Letan’s blog posts on Coq

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 Mathematical Components library and the SSReflect proof language.

Course Material

• Foundations of Separation Logic – Introduction to using separation logic to reason about sequential imperative programs in Coq.
• Introduction to Computational Logic – Introduction to basic logic principles, constructive type theory, and interactive theorem proving with Coq.

Tutorials and Hints

• CodeWars’ Coq kata – Online proving challenges.
• Coq’Art Exercises and Tutorials – Coq code and exercises from the Coq’Art book, including additional tutorials.
• Coq in a Hurry – Introduction to how Coq can be used to define logical concepts and functions and reason about them.
• Lemma Overloading – Demonstration of design patterns for programming and proving with canonical structures.
• Mike Nahas’s Coq Tutorial – Basics of using Coq to write formal proofs.
• Tricks in Coq – Tips, tricks, and features that are hard to discover.