# Track Awesome Coq Updates Daily

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

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

## Nov 14, 2022

Projects / Verified Software

- Functional Algorithms Verified in SSReflect (⭐25) - 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 (⭐15) - Library of Ltac tactics to manage and manipulate hypotheses in proofs.

## Sep 28, 2022

Resources / Course Material

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

## Aug 27, 2022

Projects / Frameworks

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

Resources / Community

## Aug 11, 2022

Projects / User Interfaces

- VsCoq (⭐203) - Extension for the Visual Studio Code and VSCodium editors.

Projects / Tools

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

## Feb 13, 2022

Projects / Verified Software

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

## Dec 19, 2021

Resources / Course Material

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

## Dec 18, 2021

Projects / Libraries

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

Projects / Tools

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

Projects / Type Theory and Mathematics

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

## Nov 29, 2021

Projects / Libraries

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

## Nov 12, 2021

Resources / Books

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

Projects / Verified Software

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

## Oct 10, 2021

Projects / Libraries

- Algebra Tactics (⭐25) - 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 (⭐27) - 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 (⭐79) - 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 (⭐50) - 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 (⭐19) - 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 (⭐37) - Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.

## Aug 15, 2021

Projects / Plugins

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

## Aug 13, 2021

Projects / Tools

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

## Aug 12, 2021

Projects / Frameworks

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

Projects / Libraries

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

Projects / Package and Build Management

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

Projects / Tools

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

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

Projects / Verified Software

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

Projects / Verified Software

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

Resources / Tutorials and Hints

- MathComp Tutorial Materials (⭐12) - 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 (⭐24) - 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 (⭐62) - Converter from Haskell code to equivalent Coq code.

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

## Oct 20, 2020

Projects / Frameworks

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

Projects / Tools

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

Projects / Type Theory and Mathematics

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

Resources / Blogs

## Sep 10, 2020

Projects / Libraries

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

Projects / Tools

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

Projects / Type Theory and Mathematics

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

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

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

- Gaia (⭐21) - 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 (⭐3) - 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 (⭐38) - Library which provides a generic way to update Coq record fields.

Projects / Plugins

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

Projects / Type Theory and Mathematics

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

## Feb 24, 2020

Projects / Libraries

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

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

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

Projects / Tools

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

Resources / Community

Resources / Blogs

## Jan 19, 2020

Projects / Frameworks

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

Projects / Libraries

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

Projects / Package and Build Management

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

Projects / Tools

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

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

## Jan 14, 2020

Projects / Type Theory and Mathematics

- Analysis (⭐138) - 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 (⭐153) - Library smoothing the transition to Coq for Haskell users.

Projects / Plugins

- AAC Tactics (⭐28) - 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 (⭐48) - Plugin adding typed tactics for backward reasoning.

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

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

Projects / Verified Software

- JSCert (⭐195) - 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 (⭐24) - 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 (⭐392) - Tips, tricks, and features that are hard to discover.

## Jan 12, 2020

Projects / Libraries

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

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

- Paco - Library for parameterized coinduction.

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

Projects / Plugins

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

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

Projects / Type Theory and Mathematics

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

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

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

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

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

Projects / Verified Software

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

- Iris - Higher-order concurrent separation logic framework.

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

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

- jsCoq (⭐0) - 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 (⭐189) - Function definition package for Coq.

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

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

Projects / Tools

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

Projects / Type Theory and Mathematics

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

Resources / Community

## Jan 09, 2020

Resources / Blogs