awesome-coq

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

Hoare Type Theory

A shallow embedding of sequential separation logic formulated as a type theory

System for reasoning using higher-order abstract syntax representations of object logics

Higher-order concurrent separation logic framework

Q*cert

Platform for implementing and verifying query compilers

SSProve

Framework for modular cryptographic proofs based on the Mathematical Components library

VCFloat

Framework for verifying C programs with floating-point computations

Verdi

Framework for formally verifying distributed systems implementations

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

Standalone graphical tool for interacting with Coq

Coqtail

Interface for Coq based on the Vim text editor

Coq LSP

Language server and extension for the Visual Studio Code and VSCodium editors with custom document checking engine

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

Company-Coq

IDE extensions for Proof General's Coq mode

opam-switch-mode

IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command

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

Language server and extension for the Visual Studio Code and VSCodium editors

VsCoq Legacy

Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol

Waterproof editor

Educational environment for writing mathematical proofs in interactive notebooks

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

Coq-Kruskal

Collection of libraries related to rose trees and Kruskal's tree theorem

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

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

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

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

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

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

Coq-related packages available in the testing distribution of Debian

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

GitHub container action that can be used with Docker-Coq or Docker-MathComp

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

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 and Coq with multiple compiler support

AAC Tactics

Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator

Coinduction

Plugin for doing proofs by enhanced coinduction

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

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

SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic

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

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

Waterproof proof language

Plugin providing a language for writing proof scripts in a style that resembles non-mechanized mathematical proof

Coqoban

Coq implementation of Sokoban, the Japanese warehouse keepers' game

Hanoi

The Tower of Hanoi puzzle in Coq, including generalizations and theorems about configurations

Mini-Rubik

Coq formalization and solver of the 2x2x2 version of the Rubik's Cube puzzle

Name the Biggest Number

Repository for submitting proven contenders for the title of biggest number in Coq

Natural Number Game

Coq version of the natural number game developed for the Lean prover

Sudoku

Formalization and solver of the Sudoku number-placement puzzle in Coq

T2048

Coq version of the 2048 sliding tile game

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

Tool for proving properties of OCaml programs in separation logic

coq2html

Alternative HTML documentation generator for Coq

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

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 (ISA) 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

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

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

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

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

CertiCoq

Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language

Fiat-Crypto

Cryptographic primitive code generation

Functional Algorithms Verified in SSReflect

Purely functional verified implementations of algorithms for searching, sorting, and other fundamental problems

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

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

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

Stable sort algorithms in Coq

Generic and modular proofs of correctness, including stability, of mergesort functions

Tarjan and Kosaraju

Verified implementations of algorithms for topological sorting and finding strongly connected components in finite graphs

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

WasmCert-Coq

Formalization in Coq of the WebAssembly (aka Wasm) 1.0 specification

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

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

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

Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis

Introduction to using separation logic to reason about sequential imperative programs in Coq

Floating-Point Numbers and Formal Proof

Introductory course on Coq real numbers and floating-point numbers from the Flocq library

Formalization to support an undergraduate course on the theory of computation, including languages and Turing machines

Lectures on Software Foundations

Material on the Software Foundations series of textbooks, including a series of YouTube videos

MathComp School

Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library

Mechanized Semantics

Companion Coq sources for a course on programming language semantics at Collège de France

Program Logics

Companion Coq sources for a course on program logics at Collège de France

Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen

Introduction to developing and verifying programs with Coq

Coq'Art Exercises and Tutorials

Coq code and exercises from the Coq'Art book, including additional tutorials

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

Guide on how to write readable and reviewable Coq code in high assurance applications

Guide to Coq tactics with explanations and examples

Whirlwind tour of Coq as a language

Lemma Overloading

Demonstration of design patterns for programming and proving with canonical structures

MathComp Tutorial Materials

Source code for Mathematical Components tutorials

Basics of using Coq to write formal proofs

Tricks in Coq

Tips, tricks, and features in Coq that are hard to discover