Coq

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

Library for reasoning on randomized algorithms.

Collection of tools for writing technical documents that mix Coq code and prose.

Ring and field tactics for Mathematical Components.

Library for classical real analysis compatible with Mathematical Components.

Tool that generates Coq code for handling binders in syntax, such as for renaming and substitutions.

Library for reasoning on fixed precision machine words.

Library of arbitrarily large numbers.

Axiom-free formalization of category theory.

Verified hash-based approximate membership structures such as Bloom filters.

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

Library for reasoning about directed graphs and their embedding in separation logic.

Tool for proving properties of OCaml programs in separation logic.

Plugin for doing proofs by enhanced coinduction.

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

IDE extensions for Proof General's Coq mode.

High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.

Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL.

Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages.

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

Nix helper scripts to automate local builds and continuous integration for Coq.

Collection of Coq packages based on opam.

Curated collection of packages to support Coq use in industry, education, and research.

Library which provides a generic way to update Coq record fields.

Templates for generating configuration files for Coq projects.

Tool for building dependency graphs between Coq objects.

Extension framework based on λProlog providing an extensive API to implement commands and tactics.

Library smoothing the transition to Coq for Haskell users.

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

Scripts for dealing with Coq files, including tabulating proof times.

Extended alternative standard library for Coq.

Scripts for manipulating Coq developments.

Alternative HTML documentation generator for Coq.

Standard documentation tool that generates LaTeX or HTML files from Coq code.

Framework to ease change of data representations in proofs.

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.

Standalone graphical tool for interacting with Coq.

Tactics for performing proofs of inequalities on expressions of real numbers.

Coq implementation of Sokoban, the Japanese warehouse keepers' game.

Tool for generating idiomatic Coq from OCaml code.

Library for certifying primality using Pocklington and Elliptic Curve certificates.

Interface for Coq based on the Vim text editor.

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.

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

Library of constructive real analysis and algebra.

Automated solver for reasoning about SQL query equivalences.

Coq-related packages available in the testing distribution of Debian.

Docker images for many versions of Coq.

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

Docker images for many combinations of versions of Coq and the Mathematical Components library.

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

Function definition package for Coq.

Collection of theories and plugins that may be useful in other Coq developments.

Framework for proofs of cryptography.

Formalization of partial commutative monoids as used in verification of pointer-manipulating programs.

Mostly automated synthesis of correct-by-construction programs.

Cryptographic primitive code generation.

Extension of Mathematical Components with finite maps, sets, and multisets.

Formalization of floating-point numbers and computations.

Library of undecidable problems and reductions between them.

Formal proof of the Four Color Theorem, a landmark result of graph theory.

Framework for modularly verifying programs with effects and effect handlers.

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

Implementation of books from Bourbaki's Elements of Mathematics, including set theory and number theory.

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

Formalization of geometry based on Tarski's axiom system.

Formalized graph theory results.

Library for reasoning on lists and binary relations.

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

Collection of commands for declaring Coq hierarchies based on packed classes.

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

Development of homotopy-theoretic ideas.

Converter from Haskell code to equivalent Coq code.

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

Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.

Formalization of information theory and linear error-correcting codes.

Library for representing recursive and impure programs.

Higher-order concurrent separation logic framework.

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

Formalized language and verified compiler for high-assurance and high-speed cryptography.

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

Port of Coq to JavaScript, which enables running Coq projects in a browser.

Coq support for the Jupyter Notebook web environment.

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

Library of Ltac tactics to manage and manipulate hypotheses in proofs.

Tool for generating locally nameless Coq definitions and proofs.

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

Abstract interfaces for mathematical structures based on type classes.

Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption.

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

Mutation analysis tool for Coq projects.

Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions.

Parser generator that can output Coq code for verified parsers.

Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins.

Library for programming language metatheory using locally nameless variable binding representations.

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

Monadic effects and equational reasoning.

Plugin adding typed tactics for backward reasoning.

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

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

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

Collection of Coq-related packages for Nix.

Formal proof of the Odd Order Theorem, a landmark result of finite group theory.

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

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

Tool for writing definitions of programming languages and calculi that can be translated to Coq.

Library for parameterized coinduction.

Plugin to generate parametricity translations of Coq terms.

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

Definitions and proofs for real-time system schedulability analysis.

Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series.

Set of bindings and libraries for interacting with Coq from inside Python 3.

Plugin for randomized property-based testing.

Platform for implementing and verifying query compilers.

Translations between different definitions of regular languages, including regular expressions and automata.

Modular formalization of algebras with heterogeneous binary relations as models.

Definition of the RISC-V processor instruction set architecture and extensions.

Tool for suggesting lemma names in Coq projects.

Tool for specifying instruction set architecture (ISA) semantics of processors and generating Coq definitions.

Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions.

Input/output monad with user-definable primitive operations.

Tool that checks proof witnesses coming from external SAT and SMT solvers.

Framework for modular cryptographic proofs based on the Mathematical Components library.

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

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

Coq version of the 2048 sliding tile game.

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.

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

Non-constructive alternative to Coq's standard library.

Generic goal preprocessing tool for proof automation tactics.

Plugin that replaces the existing unification algorithm with an enhanced one.

Library which aims to formalize a substantial body of mathematics using the univalent point of view.

Framework for verifying C programs with floating-point computations.

Verified compiler for a Lustre/Scade-like dataflow synchronous language.

Framework for formally verifying distributed systems implementations.

Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.

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

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

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.

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

Educational environment for writing mathematical proofs in interactive notebooks.

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

Processes source files to make loading of dependencies robust against shadowing of file names.

Automatically minimizes source files producing an error, creating small test cases for Coq bugs.

Creates stand-alone source files from developments by inlining the loading of all dependencies.

Removes loading of unused dependencies.

Moves all dependency loading statements to the top of source files.

Lifts many vernacular commands and inner lemmas out of proof script blocks.

Modifies source files to include proof annotations for faster parallel proving.