# Awesome

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

## 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 correct-by-construction 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 higher-order abstract syntax representations of object logics.
- Iris - Higher-order concurrent separation logic framework.
- Q*cert - Platform for implementing and verifying query compilers.
- SSProve - Framework for modular cryptographic proofs based on the Mathematical Components library.
- VCFloat - Framework for verifying C programs with floating-point computations.
- 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.
- Coq LSP - Language server and extension for the Visual Studio Code and VSCodium editors with custom document checking engine.
- 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.
- opam-switch-mode - IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command.
- 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 - Language server and extension for the Visual Studio Code and VSCodium editors.
- VsCoq Legacy - Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol.
- Waterproof editor - Educational environment for writing mathematical proofs in interactive notebooks.

### 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, 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-Kruskal - Collection of libraries related to rose trees and Kruskal's tree theorem.
- 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.
- 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 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 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 - Collection of Coq packages based on opam.
- 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.
- Debian Coq packages - Coq-related packages available in the testing distribution of Debian.
- 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 OCaml and Coq (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 and Coq with multiple compiler support.

### Plugins

- AAC Tactics - Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.
- Coinduction - Plugin for doing proofs by enhanced coinduction.
- 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.
- Itauto - SMT-like 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 property-based 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.
- Waterproof proof language - Plugin providing a language for writing proof scripts in a style that resembles non-mechanized mathematical proof.

### 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.
- Mini-Rubik - 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 number-placement puzzle in Coq.
- T2048 - Coq version of the 2048 sliding tile game.

### 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.
- 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 (ISA) semantics of processors and generating Coq definitions.
- SerAPI - Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions.
- 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 - 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.
- 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 - 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.
- CertiCoq - Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language.
- Fiat-Crypto - 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 high-assurance and high-speed cryptography.
- 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.
- Prosa - Definitions and proofs for real-time system schedulability analysis.
- RISC-V Specification in Coq - Definition of the RISC-V processor instruction set architecture and extensions.
- Stable sort algorithms in Coq - Generic and modular proofs of correctness, including stability, of mergesort functions.
- 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/Scade-like dataflow synchronous language.
- Verdi Raft - Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.
- WasmCert-Coq - Formalization in Coq of the WebAssembly (aka Wasm) 1.0 specification.

## 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 X/Twitter
- Coq Zulip chat archive
- Coq subreddit
- Coq tag on Stack Overflow
- Coq tag on Theoretical Computer Science Stack Exchange
- Coq tag on Proof Assistants Stack Exchange
- Coq keyword on Zenodo
- Coq-community package maintenance project
- Mathematical Components wiki
- 100 famous theorems proved using Coq
- Planet Coq link aggregator

### Blogs

- Coq Exchange: ideas and experiment reports about Coq
- Gagallium
- Gregory Malecha's blog
- Joachim Breitner's blog posts on Coq
- Lysxia's blog
- 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.
- 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 in-progress book and library on Kirby and Paris' hydra battles and other entertaining formalized mathematics in Coq, including a proof of the Gödel-Rosser first incompleteness theorem.

### Course Material

- An Introduction to MathComp-Analysis - Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis.
- Foundations of Separation Logic - Introduction to using separation logic to reason about sequential imperative programs in Coq.
- Floating-Point Numbers and Formal Proof - Introductory course on Coq real numbers and floating-point numbers from the Flocq library.
- Introduction to the Theory of Computation - Formalization to support an undergraduate course on the theory of computation, including languages and Turing machines.
- Lectures on Software Foundations - Material on the Software Foundations series of textbooks, including a series of YouTube videos.
- MathComp School - Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library.
- Mechanized Semantics - Companion Coq sources for a course on programming language semantics at Collège de France.
- Program Logics - Companion Coq sources for a course on program logics at Collège de France.
- Program verification with types and logic - Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.
- Proofs and Reliable Programming using Coq - Introduction to developing and verifying programs with Coq.

### Tutorials and Hints

- 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.
- Coq Tactics in Plain English - Guide to Coq tactics with explanations and examples.
- Learn X in Y minutes where X=Coq - Whirlwind tour of Coq as a language.
- 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 in Coq that are hard to discover.