Track Awesome Coq Updates Weekly
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 - Aug 18, 2024
Resources / Tutorials and Hints
- Learn X in Y minutes where X=Coq - Whirlwind tour of Coq as a language.
Jul 29 - Aug 04, 2024
Resources / Community
Jul 22 - Jul 28, 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 - Jul 21, 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 01 - 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.
Apr 29 - 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 04 - Mar 10, 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 12 - Feb 18, 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 06 - Nov 12, 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 16 - Oct 22, 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 - Sep 17, 2023
Resources / Course Material
- Program Logics (⭐37) - Companion Coq sources for a course on program logics at Collège de France.
Aug 28 - Sep 03, 2023
Projects / Frameworks
- SSProve (⭐56) - Framework for modular cryptographic proofs based on the Mathematical Components library.
Jun 12 - Jun 18, 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 22 - May 28, 2023
Resources / Blogs
Jan 02 - Jan 08, 2023
Projects / Frameworks
- Hoare Type Theory (⭐67) - A shallow embedding of sequential separation logic formulated as a type theory.
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 12 - Dec 18, 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 05 - 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 - Nov 20, 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 17 - 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 03 - Oct 09, 2022
Projects / Libraries
- LibHyps (⭐20) - Library of Ltac tactics to manage and manipulate hypotheses in proofs.
Sep 26 - Oct 02, 2022
Resources / Course Material
- Lectures on Software Foundations (⭐106) - Material on the Software Foundations series of textbooks, including a series of YouTube videos.
Aug 22 - Aug 28, 2022
Projects / Frameworks
- VCFloat (⭐21) - Framework for verifying C programs with floating-point computations.
Resources / Community
Aug 08 - Aug 14, 2022
Projects / Tools
- PyCoq (⭐50) - Set of bindings and libraries for interacting with Coq from inside Python 3.
Resources / Community
Resources / Blogs
Jun 06 - Jun 12, 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.
May 30 - Jun 05, 2022
Projects / Frameworks
- ConCert (⭐112) - Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages.
Mar 21 - Mar 27, 2022
Projects / Plugins
- Itauto - SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.
Mar 07 - Mar 13, 2022
Projects / Type Theory and Mathematics
- Four Color Theorem (⭐157) - Formal proof of the Four Color Theorem, a landmark result of graph theory.
Feb 07 - Feb 13, 2022
Projects / Verified Software
- Jasmin (⭐244) - Formalized language and verified compiler for high-assurance and high-speed cryptography.
Dec 13 - Dec 19, 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.
Resources / Course Material
- Floating-Point Numbers and Formal Proof (⭐7) - Introductory course on Coq real numbers and floating-point numbers from the Flocq library.
Nov 29 - Dec 05, 2021
Projects / Libraries
- CertiGraph (⭐16) - Library for reasoning about directed graphs and their embedding in separation logic.
Nov 08 - Nov 14, 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 01 - Nov 07, 2021
Projects / Libraries
- CoqInterval - Tactics for performing proofs of inequalities on expressions of real numbers.
- 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.
Oct 25 - Oct 31, 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 04 - Oct 10, 2021
Projects / Libraries
- Algebra Tactics (⭐29) - Ring and field tactics for Mathematical Components.
- 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.
Projects / Verified Software
- Prosa - Definitions and proofs for real-time system schedulability analysis.
Sep 06 - Sep 12, 2021
Resources / Community
Aug 23 - Aug 29, 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 16 - Aug 22, 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 09 - Aug 15, 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.
- 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 / Plugins
- Coq-Elpi (⭐134) - Extension framework based on λProlog providing an extensive API to implement commands and tactics.
Projects / Tools
- Alectryon (⭐226) - Collection of tools for writing technical documents that mix Coq code and prose.
- 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.
- SerAPI (⭐128) - Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions.
Projects / Verified Software
- Ceramist (⭐122) - Verified hash-based approximate membership structures such as Bloom filters.
- 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.
Resources / Tutorials and Hints
- MathComp Tutorial Materials (⭐17) - Source code for Mathematical Components tutorials.
Dec 07 - Dec 13, 2020
Projects / Package and Build Management
- Nix Coq packages - Collection of Coq-related packages for Nix.
Nov 30 - Dec 06, 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 26 - Nov 01, 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 14 - Sep 20, 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 24 - Aug 30, 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
Jun 01 - Jun 07, 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 23 - Mar 29, 2020
Projects / Verified Software
- Incremental Cycles - Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.
Resources / Community
Mar 02 - Mar 08, 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 / Package and Build Management
- Docker-MathComp (⭐6) - Docker images for many combinations of versions of Coq and the Mathematical Components library.
Projects / Plugins
- Ltac2 - Experimental typed tactic language similar to Coq's classic Ltac language.
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 - Mar 01, 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 10 - Feb 16, 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 20 - Jan 26, 2020
Projects / Frameworks
- CoqEAL (⭐64) - Framework to ease change of data representations in proofs.
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.
Projects / Libraries
- coq-haskell (⭐164) - Library smoothing the transition to Coq for Haskell users.
- 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 / 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
- lngen (⭐30) - Tool for generating locally nameless Coq definitions and proofs.
- Menhir - Parser generator that can output Coq code for verified parsers.
- mCoq (⭐28) - Mutation analysis tool for Coq projects.
Projects / Type Theory and Mathematics
- Analysis (⭐193) - Library for classical real analysis compatible with Mathematical Components.
- Category Theory in Coq (⭐741) - Axiom-free formalization of category theory.
- Coquelicot - Formalization of classical real analysis compatible with the standard library and focusing on usability.
- 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 / 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.
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 13 - Jan 19, 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.
- 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.
- Equations (⭐219) - Function definition package for Coq.
- MetaCoq (⭐367) - Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins.
- Paramcoq (⭐44) - Plugin to generate parametricity translations of Coq terms.
- QuickChick (⭐246) - Plugin for randomized property-based testing.
- Unicoq (⭐49) - Plugin that replaces the existing unification algorithm with an enhanced one.
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.
- 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
- 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.
- 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.
- Verdi Raft (⭐180) - Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.
Resources / Community
Resources / Blogs