Curated list of awesome lists
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 semiinteractive development of machinechecked proofs.
Contributions welcome! Read the contribution guidelines first.
Contents
Projects
Frameworks

ConCert  Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages.

CoqEAL  Framework to ease change of data representations in proofs.

FCF  Framework for proofs of cryptography.

Fiat  Mostly automated synthesis of correctbyconstruction programs.

FreeSpec  Framework for modularly verifying programs with effects and effect handlers.

Hoare Type Theory  A shallow embedding of sequential separation logic formulated as a type theory.

Hybrid  System for reasoning using higherorder abstract syntax representations of object logics.

Iris  Higherorder concurrent separation logic framework.

Q*cert  Platform for implementing and verifying query compilers.

VCFloat  Framework for verifying C programs with floatingpoint computations.

Verdi  Framework for formally verifying distributed systems implementations.

VST  Toolchain for verifying C code inside Coq in a higherorder 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.

CompanyCoq  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 and VSCodium editors.
Libraries

ALEA  Library for reasoning on randomized algorithms.

Algebra Tactics  Ring and field tactics for Mathematical Components.

Bignums  Library of arbitrarily large numbers.

Bedrock Bit Vectors  Library for reasoning on fixed precision machine words.

CertiGraph  Library for reasoning about directed graphs and their embedding in separation logic.

CoLoR  Library on rewriting theory, lambdacalculus and termination, with sublibraries on common data structures extending the Coq standard library.

coqhaskell  Library smoothing the transition to Coq for Haskell users.

CoqInterval  Tactics for performing proofs of inequalities on expressions of real numbers.

Coq record update  Library which provides a generic way to update Coq record fields.

Coqstd++  Extended alternative standard library for Coq.

ExtLib  Collection of theories and plugins that may be useful in other Coq developments.

FCSLPCM  Formalization of partial commutative monoids as used in verification of pointermanipulating programs.

Flocq  Formalization of floatingpoint numbers and computations.

Formalised Undecidable Problems  Library of undecidable problems and reductions between them.

Hahn  Library for reasoning on lists and binary relations.

Interaction Trees  Library for representing recursive and impure programs.

LibHyps  Library of Ltac tactics to manage and manipulate hypotheses in proofs.

MathComp Extra  Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption.

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.

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 userdefinable primitive operations.

TLC  Nonconstructive 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  Collection of Coq packages based on opam.

Coq Platform  Curated collection of packages to support Coq use in industry, education, and research.

coqcommunity Templates  Templates for generating configuration files for Coq projects.

DockerCoq  Docker images for many versions of Coq.

DockerMathComp  Docker images for many combinations of versions of Coq and the Mathematical Components library.

DockerCoq GitHub Action  GitHub container action that can be used with DockerCoq or DockerMathComp.

Dune  Composable and opinionated build system for OCaml and Coq (former jbuilder).

Nix  Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks.

Nix Coq packages  Collection of Coqrelated packages for Nix.

opam  Flexible and Gitfriendly package manager for OCaml and Coq with multiple compiler support.
Plugins

AAC Tactics  Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.

CoqElpi  Extension framework based on λProlog providing an extensive API to implement commands and tactics.

CoqHammer  Generalpurpose 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 floatingpoint arithmetic and roundoff errors.

Hierarchy Builder  Collection of commands for declaring Coq hierarchies based on packed classes.

Itauto  SMTlike tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.

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 propertybased testing.

SMTCoq  Tool that checks proof witnesses coming from external SAT and SMT solvers.

Tactician  Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully.

Unicoq  Plugin that replaces the existing unification algorithm with an enhanced one.
Puzzles and Games

Coqoban  Coq implementation of Sokoban, the Japanese warehouse keepers' game.

Hanoi  The Tower of Hanoi puzzle in Coq, including generalizations and theorems about configurations.

MiniRubik  Coq formalization and solver of the 2x2x2 version of the Rubik's Cube puzzle.

Name the Biggest Number  Repository for submitting proven contenders for the title of biggest number in Coq.

Natural Number Game  Coq version of the natural number game developed for the Lean prover.

Sudoku  Formalization and solver of the Sudoku numberplacement puzzle in Coq.

T2048  Coq version of the 2048 sliding tile game.

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.

coqdpdgraph  Tool for building dependency graphs between Coq objects.

coqscripts  Scripts for dealing with Coq files, including tabulating proof times.

coqtools  Scripts for manipulating Coq developments.

findbug.py
 Automatically minimizes source files producing an error, creating small test cases for Coq bugs.

absolutizeimports.py
 Processes source files to make loading of dependencies robust against shadowing of file names.

inlineimports.py
 Creates standalone source files from developments by inlining the loading of all dependencies.

minimizerequires.py
 Removes loading of unused dependencies.

moverequires.py
 Moves all dependency loading statements to the top of source files.

movevernaculars.py
 Lifts many vernacular commands and inner lemmas out of proof script blocks.

proofusinghelper.py
 Modifies source files to include proof annotations for faster parallel proving.

Cosette  Automated solver for reasoning about SQL query equivalences.

hstocoq  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.

PyCoq  Set of bindings and libraries for interacting with Coq from inside Python 3.

Roosterize  Tool for suggesting lemma names in Coq projects.

Sail  Tool for specifying instruction set architecture semantics of processors and generating Coq definitions.

SerAPI  Tools and OCaml library for (de)serialization of Coq code to and from JSON and Sexpressions.

Trakt  Generic goal preprocessing tool for proof automation tactics.
Type Theory and Mathematics

Analysis  Library for classical real analysis compatible with Mathematical Components.

Category Theory in Coq  Axiomfree 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 homotopytheoretic ideas.

Infotheo  Formalization of information theory and linear errorcorrecting codes.

Mathematical Components  Formalization of mathematical theories, focusing in particular on group theory.

Math Classes  Abstract interfaces for mathematical structures based on type classes.

Monae  Monadic effects and equational reasoning.

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  Highassurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISCV and x86 processors.

Ceramist  Verified hashbased approximate membership structures such as Bloom filters.

FiatCrypto  Cryptographic primitive code generation.

Functional Algorithms Verified in SSReflect  Purely functional verified implementations of algorithms for searching, sorting, and other fundamental problems.

Incremental Cycles  Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.

Jasmin  Formalized language and verified compiler for highassurance and highspeed cryptography.

JSCert  Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter.

lambdarust  Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries.

Prosa  Definitions and proofs for realtime system schedulability analysis.

RISCV Specification in Coq  Definition of the RISCV processor instruction set architecture and extensions.

Tarjan and Kosaraju  Verified implementations of algorithms for topological sorting and finding strongly connected components in finite graphs.

Vélus  Verified compiler for a Lustre/Scadelike dataflow synchronous language.

Verdi Raft  Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.
Resources
Blogs
Books

Coq'Art  The first book dedicated to Coq.

Software Foundations  Series of Coqbased 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 practicallyoriented 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 floatingpoint 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.

Hydras & Co.  Continuously inprogress book and library on Kirby and Paris' hydra battles and other entertaining formalized mathematics in Coq, including a proof of the GödelRosser first incompleteness theorem.
Course Material
Tutorials and Hints