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.

Contributions welcome! Read the contribution guidelines first.

Projects
Resources

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.
Hybrid - System for reasoning using higher-order abstract syntax representations of object logics.
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 arbitrarily 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.
Mczify - Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions.
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 Nix Toolbox - Nix helper scripts to automate local builds and continuous integration for Coq.
Coq Package Index - OPAM-based collection of Coq packages.
Coq platform - 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 GitHub 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 - Extension framework based on λProlog providing an extensive API to implement commands and tactics.
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

Alectryon - Collection of tools for writing technical documents that mix Coq code and prose.
Autosubst 2 - Tool that generates Coq code for handling binders in syntax, such as for renaming and substitutions.
CFML - Tool for proving properties of OCaml programs in separation logic.
coq2html - Alternative HTML documentation generator for Coq.
coqdoc - Standard documentation tool that generates LaTeX or HTML files from Coq code.
CoqOfOCaml - Tool for generating idiomatic Coq from OCaml code.
coq-dpdgraph - Tool for building dependency graphs between Coq objects.
coq-scripts - Scripts for dealing with Coq files, including tabulating proof times.
coq-tools - Scripts for manipulating Coq developments.
- find-bug.py - Automatically minimizes source files producing an error, creating small test cases for Coq bugs.
- absolutize-imports.py - Processes source files to make loading of dependencies robust against shadowing of file names.
- inline-imports.py - Creates stand-alone source files from developments by inlining the loading of all dependencies.
- minimize-requires.py - Removes loading of unused dependencies.
- move-requires.py - Moves all dependency loading statements to the top of source files.
- move-vernaculars.py - Lifts many vernacular commands and inner lemmas out of proof script blocks.
- proof-using-helper.py - Modifies source files to include proof annotations for faster parallel proving.
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 - Tools and OCaml library 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.
Goedel - Constructive proof of the Gödel-Rosser incompleteness theorem.
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.
Ceramist - Verified hash-based approximate membership structures such as Bloom filters.
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.
RISC-V Specification in Coq - Definition of the RISC-V processor instruction set architecture and extensions.
Vélus - Verified compiler for a Lustre/Scade-like dataflow synchronous language.
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 Mathematical Components library and the SSReflect proof language.
Modeling and Proving in Computational Type Theory - Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.

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.
Proofs and reliable programming using Coq - Introduction to developing and verifying programs 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.
Coq requirements in Common Criteria evaluations - Guide on how to write readable and reviewable Coq code in high assurance applications.
Hydra battles and Cie - Variations on Kirby and Paris’ hydra battles and other entertaining math in Coq, including documentation and exercises.
Lemma Overloading - Demonstration of design patterns for programming and proving with canonical structures.
MathComp Tutorial Materials - Source code for Mathematical Components tutorials.
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.