# Track Awesome Coq Updates Daily

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

🏠 Home · 🔍 Search · 🔥 Feed · 📮 Subscribe · ❤️ Sponsor · 😺 coq-community/awesome-coq · ⭐ 301 · 🏷️ Programming Languages

## Aug 12, 2024

Resources / Tutorials and Hints

- Learn X in Y minutes where X=Coq - Whirlwind tour of Coq as a language.

## Jul 29, 2024

Resources / Community

## Jul 23, 2024

Projects / Libraries

- Coq-Kruskal (⭐0) - Collection of libraries related to rose trees and Kruskal's tree theorem.

Resources / Tutorials and Hints

- Tricks in Coq (⭐491) - Tips, tricks, and features in Coq that are hard to discover.

## Jul 15, 2024

Resources / Course Material

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

## Jul 07, 2024

Projects / User Interfaces

- jsCoq (⭐507) - Port of Coq to JavaScript, which enables running Coq projects in a browser.

Projects / Plugins

- Coinduction (⭐12) - Plugin for doing proofs by enhanced coinduction.

Projects / Verified Software

- CertiCoq (⭐135) - Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language.

- Stable sort algorithms in Coq (⭐22) - Generic and modular proofs of correctness, including stability, of mergesort functions.

Resources / Tutorials and Hints

- Coq Tactics in Plain English - Guide to Coq tactics with explanations and examples.

## May 05, 2024

Resources / 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.

## Mar 05, 2024

Projects / User Interfaces

- opam-switch-mode (⭐5) - IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command.

## Feb 13, 2024

Resources / Tutorials and Hints

- Coq requirements in Common Criteria evaluations - Guide on how to write readable and reviewable Coq code in high assurance applications.

## Nov 09, 2023

Projects / User Interfaces

- VsCoq (⭐328) - Language server and extension for the Visual Studio Code and VSCodium editors.

- VsCoq Legacy (⭐328) - Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol.

Projects / Verified Software

- WasmCert-Coq (⭐89) - Formalization in Coq of the WebAssembly (aka Wasm) 1.0 specification.

Resources / Blogs

## Oct 17, 2023

Projects / User Interfaces

- Waterproof editor (⭐35) - Educational environment for writing mathematical proofs in interactive notebooks.

Projects / Package and Build Management

- Debian Coq packages - Coq-related packages available in the testing distribution of Debian.

Projects / Plugins

- Waterproof proof language (⭐29) - Plugin providing a language for writing proof scripts in a style that resembles non-mechanized mathematical proof.

## Sep 11, 2023

Resources / Course Material

- Program Logics (⭐37) - Companion Coq sources for a course on program logics at Collège de France.

## Aug 28, 2023

Projects / Frameworks

- SSProve (⭐56) - Framework for modular cryptographic proofs based on the Mathematical Components library.

## Jun 15, 2023

Projects / User Interfaces

- Coq LSP (⭐140) - Language server and extension for the Visual Studio Code and VSCodium editors with custom document checking engine.

Projects / Type Theory and Mathematics

- Homotopy Type Theory (⭐1.2k) - Development of homotopy-theoretic ideas.

## May 26, 2023

Resources / Blogs

## Jan 05, 2023

Projects / Frameworks

- Hoare Type Theory (⭐67) - A shallow embedding of sequential separation logic formulated as a type theory.

## Jan 04, 2023

Projects / Puzzles and Games

- Coqoban (⭐21) - Coq implementation of Sokoban, the Japanese warehouse keepers' game.

- Hanoi (⭐23) - The Tower of Hanoi puzzle in Coq, including generalizations and theorems about configurations.

- Mini-Rubik (⭐4) - Coq formalization and solver of the 2x2x2 version of the Rubik's Cube puzzle.

- Name the Biggest Number (⭐62) - Repository for submitting proven contenders for the title of biggest number in Coq.

- Natural Number Game (⭐6) - Coq version of the natural number game developed for the Lean prover.

- Sudoku (⭐21) - Formalization and solver of the Sudoku number-placement puzzle in Coq.

- T2048 (⭐22) - Coq version of the 2048 sliding tile game.

## Dec 16, 2022

Resources / Course Material

- MathComp School (⭐6) - Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library.

## Dec 11, 2022

Resources / Course Material

- Mechanized Semantics (⭐62) - Companion Coq sources for a course on programming language semantics at Collège de France.

## Nov 14, 2022

Projects / Verified Software

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

Resources / Community

Resources / Course Material

- Proofs and Reliable Programming using Coq - Introduction to developing and verifying programs with Coq.

## Oct 23, 2022

Projects / Tools

- Trakt (⭐14) - Generic goal preprocessing tool for proof automation tactics.

Resources / Course Material

- Introduction to the Theory of Computation - Formalization to support an undergraduate course on the theory of computation, including languages and Turing machines.

## Oct 06, 2022

Projects / Libraries

- LibHyps (⭐20) - Library of Ltac tactics to manage and manipulate hypotheses in proofs.

## Sep 28, 2022

Resources / Course Material

- Lectures on Software Foundations (⭐106) - Material on the Software Foundations series of textbooks, including a series of YouTube videos.

## Aug 27, 2022

Projects / Frameworks

- VCFloat (⭐21) - Framework for verifying C programs with floating-point computations.

Resources / Community

## Aug 11, 2022

Projects / Tools

- PyCoq (⭐50) - Set of bindings and libraries for interacting with Coq from inside Python 3.

Resources / Community

Resources / Blogs

## Jun 11, 2022

Projects / Plugins

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

## Jun 01, 2022

Projects / Frameworks

- ConCert (⭐112) - Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages.

## Mar 25, 2022

Projects / Plugins

- Itauto - SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.

## Mar 12, 2022

Projects / Type Theory and Mathematics

- Four Color Theorem (⭐157) - Formal proof of the Four Color Theorem, a landmark result of graph theory.

## Feb 13, 2022

Projects / Verified Software

- Jasmin (⭐244) - Formalized language and verified compiler for high-assurance and high-speed cryptography.

## Dec 19, 2021

Resources / Course Material

- Floating-Point Numbers and Formal Proof (⭐7) - Introductory course on Coq real numbers and floating-point numbers from the Flocq library.

## Dec 18, 2021

Projects / Libraries

- Interaction Trees (⭐198) - Library for representing recursive and impure programs.

Projects / Tools

- Sail (⭐581) - Tool for specifying instruction set architecture (ISA) semantics of processors and generating Coq definitions.

Projects / Type Theory and Mathematics

- Monae (⭐68) - Monadic effects and equational reasoning.

## Nov 29, 2021

Projects / Libraries

- CertiGraph (⭐16) - Library for reasoning about directed graphs and their embedding in separation logic.

## Nov 12, 2021

Resources / Books

- Hydras & Co. (⭐63) - 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.

## Nov 04, 2021

Projects / Libraries

- MathComp Extra (⭐5) - Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption.

Projects / Package and Build Management

- Coq Package Index - Collection of Coq packages based on opam.

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

- opam - Flexible and Git-friendly package manager for OCaml and Coq with multiple compiler support.

## Nov 03, 2021

Projects / Libraries

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

## Oct 29, 2021

Projects / Package and Build Management

- Coq Platform (⭐187) - Curated collection of packages to support Coq use in industry, education, and research.

Projects / Verified Software

- Tarjan and Kosaraju (⭐13) - Verified implementations of algorithms for topological sorting and finding strongly connected components in finite graphs.

## Oct 10, 2021

Projects / Libraries

- Algebra Tactics (⭐29) - Ring and field tactics for Mathematical Components.

Projects / Verified Software

- Prosa - Definitions and proofs for real-time system schedulability analysis.

## Oct 05, 2021

Projects / Libraries

- Bedrock Bit Vectors (⭐27) - Library for reasoning on fixed precision machine words.

- CoLoR (⭐33) - Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library.

- Flocq - Formalization of floating-point numbers and computations.

Projects / Tools

- coq-dpdgraph (⭐85) - Tool for building dependency graphs between Coq objects.

## Sep 10, 2021

Resources / Community

## Aug 25, 2021

Projects / Tools

- coq-tools (⭐37) - 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.

## Aug 21, 2021

Projects / Frameworks

- FreeSpec (⭐51) - Framework for modularly verifying programs with effects and effect handlers.

- Hybrid - System for reasoning using higher-order abstract syntax representations of object logics.

Projects / Libraries

- Mczify (⭐22) - Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions.

Projects / Tools

- coqdoc - Standard documentation tool that generates LaTeX or HTML files from Coq code.

Resources / Books

- Modeling and Proving in Computational Type Theory (⭐76) - Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.

## Aug 15, 2021

Projects / Plugins

- Coq-Elpi (⭐134) - Extension framework based on λProlog providing an extensive API to implement commands and tactics.

## Aug 13, 2021

Projects / Tools

- SerAPI (⭐128) - Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions.

## Aug 12, 2021

Projects / Frameworks

- Q*cert (⭐55) - Platform for implementing and verifying query compilers.

Projects / Libraries

- Bignums (⭐22) - Library of arbitrarily large numbers.

Projects / Package and Build Management

- Coq Nix Toolbox (⭐32) - Nix helper scripts to automate local builds and continuous integration for Coq.

Projects / Tools

- Autosubst 2 (⭐15) - Tool that generates Coq code for handling binders in syntax, such as for renaming and substitutions.

- coq-scripts (⭐8) - Scripts for dealing with Coq files, including tabulating proof times.

Projects / Verified Software

- RISC-V Specification in Coq (⭐101) - Definition of the RISC-V processor instruction set architecture and extensions.

- Vélus - Verified compiler for a Lustre/Scade-like dataflow synchronous language.

## Aug 10, 2021

Projects / Package and Build Management

- coq-community Templates (⭐12) - Templates for generating configuration files for Coq projects.

- Docker-Coq GitHub Action - GitHub container action that can be used with Docker-Coq or Docker-MathComp.

Projects / Tools

- Alectryon (⭐226) - Collection of tools for writing technical documents that mix Coq code and prose.

Projects / Verified Software

- Ceramist (⭐122) - Verified hash-based approximate membership structures such as Bloom filters.

Resources / Tutorials and Hints

- MathComp Tutorial Materials (⭐17) - Source code for Mathematical Components tutorials.

## Dec 06, 2020

Projects / Package and Build Management

- Nix Coq packages - Collection of Coq-related packages for Nix.

## Nov 23, 2020

Projects / Libraries

- Simple IO (⭐29) - Input/output monad with user-definable primitive operations.

Projects / Package and Build Management

- coq_makefile - Build tool distributed with Coq and based on generating a makefile.

Projects / Tools

- hs-to-coq (⭐77) - Converter from Haskell code to equivalent Coq code.

- Roosterize (⭐18) - Tool for suggesting lemma names in Coq projects.

## Oct 20, 2020

Projects / Frameworks

- FCF (⭐48) - Framework for proofs of cryptography.

Projects / Tools

- Ott (⭐335) - Tool for writing definitions of programming languages and calculi that can be translated to Coq.

Projects / Type Theory and Mathematics

- Coqtail Math (⭐15) - Library of mathematical results ranging from arithmetic to real and complex analysis.

Resources / Blogs

## Sep 10, 2020

Projects / Libraries

- TLC (⭐37) - Non-constructive alternative to Coq's standard library.

Projects / Tools

- coq2html (⭐28) - Alternative HTML documentation generator for Coq.

Projects / Type Theory and Mathematics

- Completeness and Decidability of Modal Logic Calculi (⭐8) - Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL.

- CoqPrime (⭐38) - Library for certifying primality using Pocklington and Elliptic Curve certificates.

- Finmap (⭐46) - Extension of Mathematical Components with finite maps, sets, and multisets.

- Gaia (⭐27) - Implementation of books from Bourbaki's Elements of Mathematics, including set theory and number theory.

Resources / Community

Resources / Books

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

Resources / Course Material

- Foundations of Separation Logic - Introduction to using separation logic to reason about sequential imperative programs in Coq.

## Aug 19, 2020

Projects / Type Theory and Mathematics

- Puiseuxth (⭐4) - Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series.

Resources / Community

## May 31, 2020

Projects / Libraries

- Coq record update (⭐42) - Library which provides a generic way to update Coq record fields.

Projects / Plugins

- Hierarchy Builder (⭐95) - Collection of commands for declaring Coq hierarchies based on packed classes.

Projects / Type Theory and Mathematics

- Graph Theory (⭐32) - Formalized graph theory results.

Resources / Community

## Mar 20, 2020

Projects / Verified Software

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

Resources / Community

## Feb 26, 2020

Projects / Package and Build Management

- Docker-MathComp (⭐6) - Docker images for many combinations of versions of Coq and the Mathematical Components library.

Projects / Type Theory and Mathematics

- Infotheo (⭐64) - Formalization of information theory and linear error-correcting codes.

Resources / Books

- The Mathematical Components book - Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.

Resources / Tutorials and Hints

- Coq'Art Exercises and Tutorials (⭐105) - Coq code and exercises from the Coq'Art book, including additional tutorials.

## Feb 24, 2020

Projects / Libraries

- Formalised Undecidable Problems (⭐102) - Library of undecidable problems and reductions between them.

- Regular Language Representations (⭐42) - Translations between different definitions of regular languages, including regular expressions and automata.

Projects / Plugins

- Ltac2 - Experimental typed tactic language similar to Coq's classic Ltac language.

## Feb 20, 2020

Projects / Package and Build Management

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

Projects / Tools

- CFML - Tool for proving properties of OCaml programs in separation logic.

## Feb 07, 2020

Projects / Libraries

- ALEA (⭐24) - Library for reasoning on randomized algorithms.

- Hahn (⭐29) - Library for reasoning on lists and binary relations.

Projects / Tools

- Cosette (⭐658) - Automated solver for reasoning about SQL query equivalences.

Resources / Community

Resources / Blogs

## Jan 19, 2020

Projects / Frameworks

- CoqEAL (⭐64) - Framework to ease change of data representations in proofs.

Projects / Libraries

- Metalib (⭐71) - Library for programming language metatheory using locally nameless variable binding representations.

Projects / Package and Build Management

- Docker-Coq (⭐37) - Docker images for many versions of Coq.

Projects / Tools

- lngen (⭐30) - Tool for generating locally nameless Coq definitions and proofs.

- mCoq (⭐28) - Mutation analysis tool for Coq projects.

Resources / 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.

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

## Jan 18, 2020

Projects / User Interfaces

- Proof General - Generic interface for proof assistants based on the extensible, customizable text editor Emacs.

- Jupyter kernel for Coq (⭐94) - Coq support for the Jupyter Notebook web environment.

## Jan 14, 2020

Projects / Type Theory and Mathematics

- Analysis (⭐193) - Library for classical real analysis compatible with Mathematical Components.

- Coquelicot - Formalization of classical real analysis compatible with the standard library and focusing on usability.

## Jan 13, 2020

Projects / Libraries

- coq-haskell (⭐164) - Library smoothing the transition to Coq for Haskell users.

Projects / Plugins

- AAC Tactics (⭐29) - Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.

- Gappa - Tactic for discharging goals about floating-point arithmetic and round-off errors.

- Mtac2 (⭐51) - Plugin adding typed tactics for backward reasoning.

- SMTCoq (⭐155) - Tool that checks proof witnesses coming from external SAT and SMT solvers.

Projects / Tools

- Menhir - Parser generator that can output Coq code for verified parsers.

Projects / Type Theory and Mathematics

- Category Theory in Coq (⭐741) - Axiom-free formalization of category theory.

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

Projects / Verified Software

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

Resources / Community

Resources / Tutorials and Hints

- Coq in a Hurry - Introduction to how Coq can be used to define logical concepts and functions and reason about them.

- Lemma Overloading (⭐26) - Demonstration of design patterns for programming and proving with canonical structures.

- Mike Nahas's Coq Tutorial - Basics of using Coq to write formal proofs.

## Jan 12, 2020

Projects / Libraries

- ExtLib (⭐124) - Collection of theories and plugins that may be useful in other Coq developments.

- FCSL-PCM (⭐25) - Formalization of partial commutative monoids as used in verification of pointer-manipulating programs.

- Paco - Library for parameterized coinduction.

- Relation Algebra (⭐43) - Modular formalization of algebras with heterogeneous binary relations as models.

Projects / Plugins

- CoqHammer (⭐210) - 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.

- MetaCoq (⭐367) - Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins.

- Unicoq (⭐49) - Plugin that replaces the existing unification algorithm with an enhanced one.

Projects / Type Theory and Mathematics

- GeoCoq (⭐179) - Formalization of geometry based on Tarski's axiom system.

- Math Classes (⭐160) - Abstract interfaces for mathematical structures based on type classes.

- Odd Order Theorem (⭐24) - Formal proof of the Odd Order Theorem, a landmark result of finite group theory.

- UniMath (⭐940) - Library which aims to formalize a substantial body of mathematics using the univalent point of view.

Projects / Verified Software

- Fiat-Crypto (⭐706) - Cryptographic primitive code generation.

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

## Jan 10, 2020

Projects / Frameworks

- Fiat (⭐145) - Mostly automated synthesis of correct-by-construction programs.

- Iris - Higher-order concurrent separation logic framework.

- Verdi (⭐580) - 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.

Projects / User Interfaces

- CoqIDE - Standalone graphical tool for interacting with Coq.

- Coqtail (⭐265) - Interface for Coq based on the Vim text editor.

- Company-Coq (⭐349) - IDE extensions for Proof General's Coq mode.

Projects / Libraries

- Coq-std++ - Extended alternative standard library for Coq.

Projects / Plugins

- Equations (⭐219) - Function definition package for Coq.

- Paramcoq (⭐44) - Plugin to generate parametricity translations of Coq terms.

- QuickChick (⭐246) - Plugin for randomized property-based testing.

Projects / Tools

- CoqOfOCaml (⭐250) - Tool for generating idiomatic Coq from OCaml code.

Projects / Type Theory and Mathematics

- CoRN (⭐108) - Library of constructive real analysis and algebra.

Projects / 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.

- Verdi Raft (⭐180) - Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.

Resources / Community

## Jan 09, 2020

Resources / Blogs