On this page
Links Coq Docs UniMath - Coq library aims to formalize a substantial body of mathematics using the univalent point of view.Mathematical Components - Libraries of formalized mathematics developed using the Coq proof assistant. (GitHub )Mathematical Components book (Code )Mathematical Components compliant Analysis Library QuickChick - Randomized Property-Based Testing Plugin for Coq.CoqHammer - Automated Reasoning Hammer Tool for Coq.coq-ext-lib - Library of Coq definitions, theorems, and tactics.Tricks in Coq - Some tips, tricks, and features in Coq that are hard to discover.MetaCoq - Metaprogramming in Coq.Convert Haskell source code to Coq source code Fiat - Deductive Synthesis of Abstract Data Types in a Proof Assistant.Advent of Code 2018 in Coq (HN )Equations - Function definition package for Coq.Proofs - Selection of formal developments in Coq.My hobby: proof engineering (2017) Programs and Proofs - Lecture notes for a short course on proving/programming in Coq via SSReflect.CoqGym - Learning Environment for Theorem Proving with the Coq proof assistant.Kami - DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness.PeaCoq - Web-based front-end to the Coq proof assistant.Kami - Platform for High-Level Parametric Hardware Specification and its Modular Verification.Lean versus Coq: The cultural chasm Awesome Coq Awesome Coq 2 coq-of-ocaml - Import OCaml programs to Coq.Poleiro - Blog about Coq. (Code )Coq'Art - Coq code and exercises from the Coq'Art book.Interaction Trees - Representing Recursive and Impure Programs in Coq (2020) Formal Reasoning About Programs - In-progress, open-source book by Adam Chlipala simultaneously introducing the Coq proof assistant and techniques for proving correctness of programs. (HN ) (Web ) (MIT course )GeoCoq - Formalization of geometry in Coq.Formalizing text editors in Coq (2020) (HN )Monadic equational reasoning in Coq Coq Enhancement Proposals A Study of Clight and its Semantics Implementing and Certifying a Web Server in Coq (2020) Rewriting in Coq FreeSpec - Framework for implementing, certifying, and executing impure computations in Coq.How hard can you believe in your logic? (2020) CoqPrime - Prime numbers for Coq.coqffi - Automatically generates Coq FFI bindings to OCaml libraries.Coqtail - Library of mathematical theorems and tools proved inside the Coq proof assistant.Interaction Trees - Library for Representing Recursive and Impure Programs in Coq.Coq/SSReflect Library for Elliptic Curves Alectryon - Library to process Coq snippets embedded in documents, showing goals and messages for each Coq sentence.Cerise - Formalisation of a capability machine and principles for reasoning about security properties.coq-procrastination - Small Coq library for collecting side conditions and deferring their proof.Finite maps - Finite sets, finite maps, multisets and generic sets.Alectryon - Collection of tools for writing technical documents that mix Coq code and prose.Certified semantics for relational programming workout 100 famous theorems proved using Coq (Code )codegen plugin for Coq Coq record update library - Automatically provides a generic way to update record fields.HELIX - Formally verified operator language and rewriting engine for high-performance computing.Bits - Formalization of bitset operations in Coq with a corresponding axiomatization and extraction to OCaml native integers.Coq formalization of information theory and linear error correcting codes jsCoq - Use Coq in Your Browser. (Code )Translating My Z3 Tutorial to Coq (2021) CoqPL: Verifying a compiler through equational means (2021) Formalization of the Calculus of Constructions in Coq Coq Library of Undecidability Proofs Perennial - Verifying concurrent crash-safe systems.Coq Platform - Multi platform setup for Coq, Coq libraries and tools.Whitehead and Russell’s Principia rewritten in Coq (Code ) (HN )Algebra Tactics - Experimental reflexive tactics for ring and field expressions.Coq encoding of ZFC and formalization of the textbook Elements of Set Theory Free Theorems from Separation Logic Specifications Example of Coq Plugin using Dune - Contains a template for writing a Coq plugin using the Dune build system.Extensional Structures - Finite sets and maps for Coq with extensional equality.SSProve - Foundational framework for modular cryptographic proofs in Coq.Eliminating Reflection from Type Theory - Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory.Mechanized semantics: the Coq development PyCoq - Access Coq from Python.Mechanization of a noninterference proof via a type system for a simple imperative language with a small-step semantics in Coq Coq library formalizes dependent type theory in the style of Per Martin-Löf Hanoi tower in Coq W-in-Coq - Coq formalization of Damas-Milner type system and its algorithm W.coq-bonsai - Generate a fresh bonsai in your terminal. Written in Coq.Coq-Combi - Algebraic Combinatorics in Coq.Toy Hoare Logic Formalization for IMP Reasoning about the garden of forking paths (2021) (Coq Code )Formalization of the basic actuarial mathematics using Coq Sniper - Coq plugin that provides a new Coq tactic, snipe, that provides general proof automation.SMTCoq - Communication between Coq and SAT/SMT solvers.TLC - Library for Classical Coq.Formalization of some elementary mathematical theories in Coq Stable sort algorithms in Coq CertiCoq - Compiler for Gallina, the specification language of the Coq proof assistant.Tealeaves - Coq library for proving theorems about syntax abstractly.Connectivity Graphs Coq Development Hemiola - Coq framework to support structural design and proof of hardware cache-coherence protocols.Mczify - Micromega tactics for Mathematical Components.Hierarchy Builder - High level commands to declare a hierarchy based on packed classes.Coq Package Index - Archive for all Coq related OPAM packages organized in various repositories. (Code )Formalizing Dawn in Coq (2021) Semantics - Survey of semantics styles in Coq.vstyle - Style guide for Coq. (Docs )AAC Tactics - Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.Vermillion - LL(1) parser generator verified in Coq.Coq Domains Proof in Coq of the Gödel-Rosser 1st incompleteness theorem Coq-Elpi - Coq plugin embedding Elpi.Cheat Sheet for Coq (Code )Apery - Formal proof of the irrationality of zeta(3), the Apéry constant.Ordinal Numbers in Coq Coq development of A Promising Semantics for Relaxed-Memory Concurrency Coq Developments for Linear Types coq-ext-lib - Collection of theories and plugins that may be useful in other Coq developments.Math Classes - Library of abstract interfaces for mathematical structures in Coq.C-CoRN - Coq Repository at Nijmegen.ch2o - Aims at formalizing novel features of the ISO C11 standard of the C programming language.ATBR - Coq library and tactic for deciding Kleene algebras.Multinomials - Multivariate polynomial Library for the Mathematical Components Library.Efficient Extensional Binary Tries (2021) (Code )UniCoq - Enhanced unification algorithm for Coq.Phase Semantics - Some Coq formalizations of Linear Logic.CertiGraph - Library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.Coinduction - Library for doing proofs by (enhanced) coinduction.Tactical - Library of Coq proof automation.Huffman - Correctness proof of the Huffman coding algorithm in Coq.Nuprl's type theory in Coq Trakt - Generic goal preprocessing tool for proof automation tactics in Coq.metalib - Penn Locally Nameless Metatheory Library.Scripts associated to tutorials for mathcomp Ergo - Language for Smart Legal Contracts. (Web )Bonak - Research project that formalizes semi-cubical types in Coq.Imp: Simple Imperative Programs Monadic Coq Compiler - Alternative Coq compiler, by extraction to C++17. Written in Haskell.Noq - Simple expression transformer that is not Coq. (Dev Stream )Falso - Proof of false in Coq. (HN )ChickBlog - Blog engine written and proven in Coq.Practical Aspects of Monadic Equational Reasoning in Coq (2022) Making Weak Memory Models Fair using Coq Relation Algebra for Coq Mathematics of Rigid Body Transformationss using Coq and MathComp Country-Fried Coq: Overly- Formalized Nonstandard Arithmetic (2022) Hydras & Co - Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises).Mechanized Theory of Event Structures Few Coq typeclasses Mtac2 - Typed tactic language for Coq. (Paper )Autosubst - Library for the Coq proof assistant which provides automation for formalizing syntactic theories with variable binders.Argosy - Verifying layered storage systems with recovery refinement.Coq Performance Tests - Library of Coq source files testing for performance regressions on Coq.xmonad in Coq mCoq - Mutation analysis tool for Coq verification projects.bedrock2 - Work-in-progress language and compiler for verified low-level programming.Useful scripts for dealing with Coq files Coq Universe - Aim to provide a composed build of all active Coq developments in existence.Formal proof of the Odd Order Theorem in Coq Paramcoq - Coq plugin providing commands for generating parametricity statements.Gaia - Implementation of books from Bourbaki's Elements of Mathematics in Coq.Rupicola - Relation compilation for performance-critical applications.Coherence space semantics for linear logic in Coq Computability in Constructive Type Theory in Coq Deriving - Generic instances for Coq inductive types.Coq LSP - Language Server Protocol for Coq.CoqBan - Allows you to directly execute your Coq code uploaded to Gist.coq-switch Coqoban - Coq implementation of Sokoban, the Japanese warehouse keepers' game.Lustre compiler in Coq Choice Trees - itree-like data-structure to additionally support internal non-determinism.Automatik - Library of formalized graph and automata based algorithms.