Your first time on this page? Allow me to give some explanations.
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [[email protected],@palmskog]
Here you can see meta information about this topic like the time we last updated this page, the original creator of the awesome list and a link to the original GitHub repository.
Thank you coq-community & contributors
View Topic on GitHub:
Search for resources by name or description.
Simply type in what you are looking for and the results will be filtered on the fly.
Further filter the resources on this page by type (repository/other resource), number of stars on GitHub and time of last commit in months.
CoqEAL -- The Coq Effective Algebra Library
Foundational Cryptography Framework for machine-checked proofs of cryptography.
Mostly Automated Synthesis of Correct-by-Construction Programs
A framework for implementing and certifying impure computations in Coq
A framework for formally verifying distributed systems implementations in Coq
Interactive Coq Proofs in Vim
IDE extensions for Proof General's Coq mode
Jupyter kernel for Coq
Standalone graphical tool for interacting with Coq.
Coq library for reasoning on randomized algorithms [[email protected],@volodeyka]
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
A library for formalizing Haskell types and functions in Coq
Library to create Coq record update functions
A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
Partial Commutative Monoids
A library of mechanised undecidability proofs in the Coq proof assistant.
Hahn: A Coq library
The Penn Locally Nameless Metatheory Library
Monadic effects and equational reasonig in Coq
Relation algebra library for Coq
IO for Gallina
Library for Classical Coq
Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library.
Package and Build Management
Preliminary / experimental version of the Coq platform discussed in the coq-dev maling list.
Templates for configuration files and scripts useful for maintaining Coq projects [[email protected],@Zimmi48]
Docker images of mathcomp
Build tool distributed by Coq and based on generating a makefile.
Composable and opinionated build system for Coq and OCaml (former jbuilder).
Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks.
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [[email protected]]
Coq plugin embedding elpi
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
A function definition package for Coq
High level commands to declare a hierarchy based on packed classes
Metaprogramming in Coq
Randomized Property-Based Testing Plugin for Coq
Communication between Coq and SAT/SMT solvers
An enhanced unification algorithm for Coq
Tactic for discharging goals about floating-point arithmetic and round-off errors.
An HTML documentation generator for Coq source files
Import OCaml programs to Coq 🐓 🐫
Build dependency graphs between COQ objects
Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
Cosette is an automated SQL solver.
Convert Haskell source code to Coq source code.
Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott
Mutation analysis tool for Coq verification projects
The Ott tool for writing definitions of programming languages and calculi
Tool for suggesting lemma names in Coq verification projects
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Tool for proving properties of OCaml programs in separation logic.
Type Theory and Mathematics
Mathematical Components compliant Analysis Library
An axiom-free formalization of category theory in Coq for personal study and practical work
Completeness and Decidability of Modal Logic Calculi [[email protected]]
Prime numbers for Coq
Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis. [[email protected]]
Finite sets, finite maps, multisets and generic sets
Formal proof of the Four Color Theorem
Implementation of books from Bourbaki's Elements of Mathematics in Coq
A formalization of geometry in Coq based on Tarski's axiom system
Homotopy type theory
A Coq formalization of information theory and linear error-correcting codes
A library of abstract interfaces for mathematical structures in Coq [[email protected]]
The formal proof of the Odd Order Theorem
Formal proof in Coq of Puiseux's Theorem.
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Formalization of classical real analysis compatible with the standard library and focusing on usability.
Cryptographic Primitive Code Generation by Fiat
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.
Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners.
Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
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.
Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.
Foundations of separation logic for reasoning about sequential programs in Coq.
Tutorials and Hints
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [[email protected]]
Tricks you wish the Coq manual told you
Introduction to how Coq can be used to define logical concepts and functions and reason about them.