User Experience on mobile might not be great yet, but I'm working on it.

Your first time on this page? Allow me to give some explanations.

Awesome Coq

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.

Last Update: Nov. 24, 2020, 6:06 p.m.

Thank you coq-community & contributors
View Topic on GitHub:
coq-community/awesome-coq

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.

Frameworks

CoqEAL -- The Coq Effective Algebra Library

44
10
100d
n/a

Foundational Cryptography Framework for machine-checked proofs of cryptography.

31
20
73d
n/a

Mostly Automated Synthesis of Correct-by-Construction Programs

115
20
51d
n/a

A framework for implementing and certifying impure computations in Coq

42
7
30d
GPL-3.0

A framework for formally verifying distributed systems implementations in Coq

491
47
5m
BSD-2-Clause

Higher-order concurrent separation logic framework.

Platform for implementing and verifying query compilers.

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

Interactive Coq Proofs in Vim

98
15
7d
MIT

IDE extensions for Proof General's Coq mode

287
22
4m
GPL-3.0

A port of Coq to Javascript -- Run Coq in your Browser

368
25
10d
n/a

Jupyter kernel for Coq

45
5
9m
Apache-2.0

A Visual Studio Code extension for Coq [[email protected]]

124
21
21d
MIT

Standalone graphical tool for interacting with Coq.

Generic interface for proof assistants based on the extensible, customizable text editor Emacs.

Libraries

Coq library for reasoning on randomized algorithms [[email protected],@volodeyka]

5
0
105d
LGPL-2.1

Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library

16
14
23d
LGPL-2.1

A library for formalizing Haskell types and functions in Coq

136
10
9m
n/a

Library to create Coq record update functions

24
5
7d
MIT

A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]

96
31
77d
n/a

Partial Commutative Monoids

15
8
5d
Apache-2.0

A library of mechanised undecidability proofs in the Coq proof assistant.

41
11
5d
n/a

Hahn: A Coq library

20
8
97d
MIT

The Penn Locally Nameless Metatheory Library

45
18
6m
n/a

Monadic effects and equational reasonig in Coq

45
3
25d
LGPL-2.1

Regular Language Representations in Coq [[email protected],@palmskog]

16
2
50d
n/a

Relation algebra library for Coq

28
7
36d
n/a

IO for Gallina

18
1
2d
MIT

Library for Classical Coq

2
0
77d
n/a

Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library.

Extended alternative standard library for Coq.

Formalization of floating-point computations.

Library for parameterized coinduction.

Package and Build Management

Preliminary / experimental version of the Coq platform discussed in the coq-dev maling list.

8
2
84d
LGPL-2.1

Templates for configuration files and scripts useful for maintaining Coq projects [[email protected],@Zimmi48]

9
5
33d
Unlicense

Docker images of the Coq proof assistant [[email protected]]

20
2
9d
BSD-3-Clause

Docker images of mathcomp

4
0
89d
BSD-3-Clause

Build tool distributed by Coq and based on generating a makefile.

OPAM-based collection of Coq packages.

Composable and opinionated build system for Coq and OCaml (former jbuilder).

Nix

Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks.

Collection of Coq-related packages for Nix.

Flexible and Git-friendly package manager for OCaml with multiple compiler support.

Plugins

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [[email protected]]

17
16
10d
n/a

Coq plugin embedding elpi

43
16
6d
LGPL-2.1

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

152
19
29d
LGPL-2.1

A function definition package for Coq

151
32
5d
LGPL-2.1

High level commands to declare a hierarchy based on packed classes

35
2
22d
MIT

Metaprogramming in Coq

187
45
8d
MIT
39
14
91d
n/a

Coq plugin for parametricity [[email protected]]

32
19
8d
n/a

Randomized Property-Based Testing Plugin for Coq

178
22
111d
n/a

Communication between Coq and SAT/SMT solvers

86
21
89d
n/a

An enhanced unification algorithm for Coq

32
11
5d
MIT

Tactic for discharging goals about floating-point arithmetic and round-off errors.

Experimental typed tactic language similar to Coq's classic Ltac language.

Tools

An HTML documentation generator for Coq source files

17
6
93d
GPL-2.0

Import OCaml programs to Coq ๐Ÿ“ ๐Ÿซ

106
7
6d
MIT

Build dependency graphs between COQ objects

54
17
27d
LGPL-2.1

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

23
5
62d
MIT

Cosette is an automated SQL solver.

527
44
1y 7m
BSD-2-Clause

Convert Haskell source code to Coq source code.

19
0
7d
MIT

Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott

23
6
6m
MIT

Mutation analysis tool for Coq verification projects

16
1
6m
Apache-2.0

The Ott tool for writing definitions of programming languages and calculi

178
26
41d
n/a

Tool for suggesting lemma names in Coq verification projects

7
2
4d
MIT

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

79
18
85d
n/a

Tool for proving properties of OCaml programs in separation logic.

Menhir is a LR(1) parser generator for OCaml.

Type Theory and Mathematics

Mathematical Components compliant Analysis Library

75
13
5d
n/a

An axiom-free formalization of category theory in Coq for personal study and practical work

549
44
110d
BSD-3-Clause

Completeness and Decidability of Modal Logic Calculi [[email protected]]

2
0
76d
n/a

Prime numbers for Coq

8
9
90d
LGPL-2.1

Coq Repository at Nijmegen [[email protected],@VincentSe]

96
35
15d
GPL-2.0

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]]

5
0
37d
n/a

Finite sets, finite maps, multisets and generic sets

33
14
106d
n/a

Formal proof of the Four Color Theorem

81
11
5d
n/a

Implementation of books from Bourbaki's Elements of Mathematics in Coq

3
1
77d
MIT

A formalization of geometry in Coq based on Tarski's axiom system

124
22
33d
LGPL-3.0

Graph Theory [[email protected],@damien-pous]

4
1
5d
n/a

Homotopy type theory

926
153
16d
n/a

A Coq formalization of information theory and linear error-correcting codes

34
3
10d
LGPL-2.1

A library of abstract interfaces for mathematical structures in Coq [[email protected]]

134
38
37d
MIT

The formal proof of the Odd Order Theorem

11
10
58d
n/a

Formal proof in Coq of Puiseux's Theorem.

3
0
5m
n/a

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

660
128
7d
n/a

Formalization of classical real analysis compatible with the standard library and focusing on usability.

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

Verified Software

Cryptographic Primitive Code Generation by Fiat

278
82
16d
n/a

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

184
9
1y 7m
n/a

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

142
16
5m
BSD-2-Clause

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.

Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries.

Community

Blogs

Books

The first book dedicated to Coq.

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.

Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.

Course Material

Foundations of separation logic for reasoning about sequential programs in Coq.

Introduction to basic logic principles, constructive type theory, and interactive theorem proving with Coq.

Tutorials and Hints

Coq code and exercises from the Coq'Art book [[email protected],@Casteran]

30
7
41d
MIT

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [[email protected]]

17
7
20d
GPL-3.0

Tricks you wish the Coq manual told you

284
9
5d
n/a

Introduction to how Coq can be used to define logical concepts and functions and reason about them.