Coq

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

Framework to ease change of data representations in proofs.

Framework for proofs of cryptography.

Mostly automated synthesis of correct-by-construction programs.

Framework for modularly verifying programs with effects and effect handlers.

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

Platform for implementing and verifying query compilers.

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

Framework for verifying C programs with floating-point computations.

Framework for formally verifying distributed systems implementations.

Interface for Coq based on the Vim text editor.

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

IDE extensions for Proof General's Coq mode.

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

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

Coq support for the Jupyter Notebook web environment.

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

Educational environment for writing mathematical proofs in interactive notebooks.

Partial Rocq tree-sitter grammar useful for syntax highlighting in text editors like Helix, but not recommended for full parsing of Rocq code.

Library for reasoning on randomized algorithms.

Ring and field tactics for Mathematical Components.

Library of arbitrarily large numbers.

Library for reasoning on fixed precision machine words.

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

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

Library smoothing the transition to Coq for Haskell users.

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

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

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

Library of undecidable problems and reductions between them.

Library for reasoning on lists and binary relations.

Library for representing recursive and impure programs.

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

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

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

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

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

Modular formalization of algebras with heterogeneous binary relations as models.

Input/output monad with user-definable primitive operations.

Non-constructive alternative to Coq's standard library.

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

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

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

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

Templates for generating configuration files for Coq projects.

Docker images for many versions of Coq.

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

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

Plugin for doing proofs by enhanced coinduction.

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

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.

Function definition package for Coq.

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

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

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

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

Plugin adding typed tactics for backward reasoning.

Plugin to generate parametricity translations of Coq terms.

Plugin for randomized property-based testing.

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

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

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

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

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

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.

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

Coq version of the 2048 sliding tile game.

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

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

Alternative HTML documentation generator for Coq.

Tool for generating idiomatic Coq from OCaml code.

Tool for building dependency graphs between Coq objects.

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

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

Automated solver for reasoning about SQL query equivalences.

Converter from Haskell code to equivalent Coq code.

Tool for generating locally nameless Coq definitions and proofs.

Mutation analysis tool for Coq projects.

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

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

Fork of coq2html that adds indexes, clickable notations, Markdown and LaTeX formatting in comments, and more.

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.

Generic goal preprocessing tool for proof automation tactics.

Library for classical real analysis compatible with Mathematical Components.

Axiom-free formalization of category theory.

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

Library for certifying primality using Pocklington and Elliptic Curve certificates.

Library of constructive real analysis and algebra.

Library of mathematical results ranging from arithmetic to real and complex analysis.

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

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

Formalization of geometry based on Tarski's axiom system.

Formalized graph theory results.

Development of homotopy-theoretic ideas.

Formalization of information theory and linear error-correcting codes.

Abstract interfaces for mathematical structures based on type classes.

Monadic effects and equational reasoning.

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

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

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

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

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.

Cryptographic primitive code generation.

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

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

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

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

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

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

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

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