# Track Awesome Coq Updates Daily

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]

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

## Sep 11, 2023

Projects / Plugins

- coq-waterproof (⭐20) - Plugin for writing Coq proof scripts in a style that resembles non-mechanized mathematical proof.

Resources / Course Material

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

## Aug 28, 2023

Projects / Frameworks

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

## Jul 08, 2023

Resources / Community

## Jun 21, 2023

Projects / User Interfaces

- VsCoq1 (⭐257) - Extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol.

- VsCoq2 (⭐257) - Experimental language server and extension for the Visual Studio Code and VSCodium editors.

## Jun 15, 2023

Projects / User Interfaces

- Coq LSP (⭐100) - 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 (⭐61) - 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 (⭐3) - Coq formalization and solver of the 2x2x2 version of the Rubik's Cube puzzle.

- Name the Biggest Number (⭐51) - 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 (⭐20) - 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 (⭐5) - 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 (⭐47) - 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 (⭐32) - 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 (⭐12) - 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 (⭐16) - Library of Ltac tactics to manage and manipulate hypotheses in proofs.

## Sep 28, 2022

Resources / Course Material

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

## Aug 27, 2022

Projects / Frameworks

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

Resources / Community

## Aug 11, 2022

Projects / Tools

- PyCoq (⭐47) - 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 (⭐93) - Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages.

## May 18, 2022

Resources / Tutorials and Hints

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

## 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 (⭐132) - Formal proof of the Four Color Theorem, a landmark result of graph theory.

## Feb 13, 2022

Projects / Verified Software

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

## Dec 19, 2021

Resources / Course Material

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

## Dec 18, 2021

Projects / Libraries

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

Projects / Tools

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

Projects / Type Theory and Mathematics

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

## Nov 29, 2021

Projects / Libraries

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

## Nov 12, 2021

Resources / Books

- Hydras & Co. (⭐49) - 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 (⭐4) - 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 (⭐153) - Curated collection of packages to support Coq use in industry, education, and research.

Projects / Verified Software

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

## Oct 10, 2021

Projects / Libraries

- Algebra Tactics (⭐28) - 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 (⭐25) - Library for reasoning on fixed precision machine words.

- CoLoR (⭐30) - 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 (⭐81) - Tool for building dependency graphs between Coq objects.

## Sep 10, 2021

Resources / Community

## Aug 25, 2021

Projects / Tools

- coq-tools (⭐34) - 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 (⭐49) - 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 (⭐21) - 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 (⭐58) - Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.

## Aug 15, 2021

Projects / Plugins

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

## Aug 13, 2021

Projects / Tools

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

## Aug 12, 2021

Projects / Frameworks

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

Projects / Libraries

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

Projects / Package and Build Management

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

Projects / Tools

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

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

Projects / Verified Software

- RISC-V Specification in Coq (⭐87) - 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 (⭐11) - 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 (⭐206) - Collection of tools for writing technical documents that mix Coq code and prose.

Projects / Verified Software

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

Resources / Tutorials and Hints

- MathComp Tutorial Materials (⭐16) - 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 (⭐27) - 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 (⭐71) - Converter from Haskell code to equivalent Coq code.

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

## Oct 20, 2020

Projects / Frameworks

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

Projects / Tools

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

Projects / Type Theory and Mathematics

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

Resources / Blogs

## Sep 10, 2020

Projects / Libraries

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

Projects / Tools

- coq2html (⭐26) - 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 (⭐32) - Library for certifying primality using Pocklington and Elliptic Curve certificates.

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

- Gaia (⭐23) - 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

Resources / Blogs

## May 31, 2020

Projects / Libraries

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

Projects / Plugins

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

Projects / Type Theory and Mathematics

- Graph Theory (⭐27) - 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 (⭐60) - 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 (⭐87) - Coq code and exercises from the Coq'Art book, including additional tutorials.

## Feb 24, 2020

Projects / Libraries

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

- Regular Language Representations (⭐37) - 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 (⭐23) - Library for reasoning on randomized algorithms.

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

Projects / Tools

- Cosette (⭐635) - 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 (⭐67) - Library for programming language metatheory using locally nameless variable binding representations.

Projects / Package and Build Management

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

Projects / Tools

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

- mCoq (⭐25) - 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 (⭐86) - Coq support for the Jupyter Notebook web environment.

## Jan 14, 2020

Projects / Type Theory and Mathematics

- Analysis (⭐163) - 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 (⭐159) - 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 (⭐49) - Plugin adding typed tactics for backward reasoning.

- SMTCoq (⭐142) - 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 (⭐705) - Axiom-free formalization of category theory.

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

Projects / Verified Software

- JSCert (⭐193) - 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.

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

## Jan 12, 2020

Projects / Libraries

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

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

- Paco - Library for parameterized coinduction.

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

Projects / Plugins

- CoqHammer (⭐192) - 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 (⭐298) - Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins.

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

Projects / Type Theory and Mathematics

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

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

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

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

Projects / Verified Software

- Fiat-Crypto (⭐605) - 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 (⭐141) - Mostly automated synthesis of correct-by-construction programs.

- Iris - Higher-order concurrent separation logic framework.

- Verdi (⭐557) - 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 (⭐219) - Interface for Coq based on the Vim text editor.

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

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

Projects / Libraries

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

Projects / Plugins

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

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

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

Projects / Tools

- CoqOfOCaml (⭐216) - 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 (⭐170) - Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.

Resources / Community

## Jan 09, 2020

Resources / Blogs