Skip to content

coq-community/awesome-coq

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Awesome Coq Awesome

coq-community logo

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.
  • 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.
  • 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.
  • 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.
  • 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 - Extension for the Visual Studio Code and VSCodium editors.

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

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

Resources

Community

Blogs

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

Tutorials and Hints

About

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

Topics

Resources

License

Stars

Watchers

Forks