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: May 7, 2021, 10:38 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

47
10
90d
n/a

Foundational Cryptography Framework for machine-checked proofs of cryptography.

31
20
7m
n/a

Mostly Automated Synthesis of Correct-by-Construction Programs

117
21
74d
n/a

A framework for implementing and certifying impure computations in Coq

41
7
73d
MPL-2.0

A framework for formally verifying distributed systems implementations in Coq

494
47
10m
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

106
16
81d
MIT

IDE extensions for Proof General's Coq mode

294
23
5m
GPL-3.0

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

370
25
81d
n/a

Jupyter kernel for Coq

51
5
1y 92d
Apache-2.0

A Visual Studio Code extension for Coq [[email protected],@fakusb]

132
22
4m
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]

7
0
5m
LGPL-2.1

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

16
14
5m
LGPL-2.1

A library for formalizing Haskell types and functions in Coq

135
10
1y 88d
n/a

Library to create Coq record update functions

26
7
114d
MIT

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

100
34
100d
n/a

Partial Commutative Monoids

16
8
114d
Apache-2.0

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

47
12
98d
n/a

Hahn: A Coq library

21
8
74d
MIT

The Penn Locally Nameless Metatheory Library

47
16
11m
n/a

Monadic effects and equational reasonig in Coq

45
5
75d
LGPL-2.1

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

19
2
4m
n/a

Relation algebra library for Coq

29
8
4m
n/a

IO for Gallina

18
1
5m
MIT

Library for Classical Coq

2
0
8m
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
8m
LGPL-2.1

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

9
7
4m
Unlicense

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

25
2
4m
BSD-3-Clause

Docker images of mathcomp

4
1
4m
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.

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

18
18
4m
n/a

Coq plugin embedding elpi

50
20
74d
LGPL-2.1

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

155
20
98d
LGPL-2.1

A function definition package for Coq

157
32
85d
LGPL-2.1

High level commands to declare a hierarchy based on packed classes

37
2
73d
MIT

Metaprogramming in Coq

189
44
4m
MIT
39
14
8m
n/a

Coq plugin for parametricity [[email protected]]

32
19
105d
n/a

Randomized Property-Based Testing Plugin for Coq

186
22
109d
n/a

Communication between Coq and SAT/SMT solvers

92
23
74d
n/a

An enhanced unification algorithm for Coq

32
12
4m
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
8m
GPL-2.0

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

116
7
78d
MIT

Build dependency graphs between COQ objects

57
17
4m
LGPL-2.1

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

24
6
7m
MIT

Cosette is an automated SQL solver.

531
46
2y 34d
BSD-2-Clause

Convert Haskell source code to Coq source code.

19
0
5m
MIT

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

24
6
11m
MIT

Mutation analysis tool for Coq verification projects

16
1
11m
Apache-2.0

The Ott tool for writing definitions of programming languages and calculi

178
26
6m
n/a

Tool for suggesting lemma names in Coq verification projects

7
2
5m
MIT

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

87
21
84d
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

79
14
78d
n/a

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

560
49
108d
BSD-3-Clause

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

2
0
8m
n/a

Prime numbers for Coq

8
9
8m
LGPL-2.1

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

96
35
76d
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
6m
n/a

Finite sets, finite maps, multisets and generic sets

33
14
9m
n/a

Formal proof of the Four Color Theorem

87
13
88d
n/a

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

3
1
8m
MIT

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

124
22
6m
LGPL-3.0

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

7
1
5m
n/a

Homotopy type theory

940
155
108d
n/a

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

34
4
73d
LGPL-2.1

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

132
38
5m
MIT

The formal proof of the Odd Order Theorem

11
9
73d
n/a

Formal proof in Coq of Puiseux's Theorem.

3
0
10m
n/a

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

677
128
75d
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

352
90
73d
n/a

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

184
9
2y 30d
n/a

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

142
15
10m
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]

36
7
103d
MIT

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

17
7
115d
GPL-3.0

Tricks you wish the Coq manual told you

297
10
109d
n/a

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