uhub/awesome-coq

A curated list of awesome Coq frameworks, libraries and software.

{
  "createdAt": "2015-08-21T03:29:02Z",
  "defaultBranch": "master",
  "description": "A curated list of awesome Coq frameworks, libraries and software.",
  "fullName": "uhub/awesome-coq",
  "homepage": null,
  "language": null,
  "name": "awesome-coq",
  "pushedAt": "2025-11-19T00:01:44Z",
  "stargazersCount": 235,
  "topics": [],
  "updatedAt": "2025-11-19T00:01:47Z",
  "url": "https://github.com/uhub/awesome-coq"
}

awesome-coq

A curated list of awesome Coq frameworks, libraries and software.

AbsInt/CompCert - The CompCert formally-verified C compiler
HoTT/Coq-HoTT - A Coq library for Homotopy Type Theory
formal-land/coq-of-rust - Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦
UniMath/UniMath - This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
magmide/magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
jwiegley/category-theory - An axiom-free formalization of category theory in Coq for personal study and practical work
math-comp/math-comp - Mathematical Components
uwplse/verdi - A framework for formally verifying distributed systems implementations in Coq
rocq-community/rocq-tricks - Tricks you wish the Coq manual told you [maintainer=@tchajed]
MetaRocq/metarocq - Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
PrincetonUniversity/VST - Verified Software Toolchain
princeton-vl/CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant
jasmin-lang/jasmin - Language for high-assurance and high-speed cryptography
stepchowfun/proofs - My personal repository of formally verified mathematics.
antalsz/hs-to-coq - Convert Haskell source code to Coq source code
QuickChick/QuickChick - Randomized Property-Based Testing Plugin for Coq
mit-pdos/fscq - FSCQ is a certified file system written and proven in Coq
UniMath/Foundations - Voevodsky’s original development of the univalent foundations of mathematics in Coq
DeepSpec/InteractionTrees - A Library for Representing Recursive and Impure Programs in Coq
mattam82/Coq-Equations - A function definition package for Coq
math-comp/analysis - Mathematical Components compliant Analysis Library
rocq-community/fourcolor - Formal proof of the Four Color Theorem [maintainer=@ybertot]
sifive/Kami - Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
jscert/jscert - A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
GeoCoq/GeoCoq - A formalization of geometry in Coq based on Tarski’s axiom system
uwplse/verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
clarus/coq-chick-blog - 🐣 A blog engine written and proven in Coq
barry-jay-personal/tree-calculus - Proofs in Coq for the book Reflective Programs in Tree Calculus
LPCIC/coq-elpi - Coq plugin embedding elpi
ilyasergey/pnp - Lecture notes for a short course on proving/programming in Coq via SSReflect.
jwiegley/coq-haskell - A library for formalizing Haskell types and functions in Coq
rocq-community/math-classes - A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
mit-plv/koika - A core language for rule-based hardware design 🦑
mit-plv/kami - A Platform for High-Level Parametric Hardware Specification and its Modular Verification
CertiCoq/certicoq - A Verified Compiler for Gallina, Written in Gallina
discus-lang/iron - Coq formalizations of functional languages.
Lysxia/advent-of-coq-2018 - Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
rocq-community/coq-ext-lib - A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
rocq-archive/coq-serapi - Coq Protocol Playground with Se(xp)rialization of Internal Structures.
rocq-community/coq-art - Coq code and exercises from the Coq’Art book [maintainers=@ybertot,@Casteran]
project-oak/silveroak - Formal specification and verification of hardware, especially for security and privacy.
uds-psl/coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
verse-lab/ceramist - Verified hash-based AMQ structures in Coq
AU-COBRA/ConCert - A framework for smart contract verification in Coq
mit-plv/riscv-coq - RISC-V Specification in Coq
rocq-community/corn - Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
verse-lab/toychain - A minimalistic blockchain consensus implemented and verified in Coq
WasmCert/WasmCert-Coq - A mechanisation of Wasm in Coq(Rocq)
Ptival/PeaCoq - PeaCoq is a pretty Coq, isn’t it?
math-comp/hierarchy-builder - High level commands to declare a hierarchy based on packed classes
DistributedComponents/disel - Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
clarus/falso - A proof of false in Coq.
amintimany/Categories - A formalization of category theory in the Coq proof assistant.
sec-bit/tokenlibs-with-proofs - Correctness proofs of Ethereum token contracts
ymherklotz/vericert - A formally verified high-level synthesis tool based on CompCert and written in Coq.
rocq-community/coq-dpdgraph - Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
plclub/hs-to-coq - Convert Haskell source code to Coq source code.
neelsomani/cuq - Cuq: A MIR-to-Coq Framework Targeting PTX for Formal Semantics and Verified Translation of Rust GPU Kernels
coq-concurrency/pluto - A web server written in Coq.
inQWIRE/SQIR - A Small Quantum Intermediate Representation
SkylabsAI/BRiCk - Formalization of C++ for verification purposes.
pi8027/lambda-calculus - A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
imdea-software/htt - Hoare Type Theory
rocq-community/hydra-battles - Variations on Kirby & Paris’ hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
ml4tp/gamepad - A Learning Environment for Theorem Proving
rocq-community/coqeal - The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
INRIA/velus - A Lustre compiler in Coq
SSProve/ssprove - A foundational framework for modular cryptographic proofs in Coq
rocq-archive/coq-in-coq - A formalisation of the Calculus of Constructions
xavierleroy/cdf-mech-sem - Coq development for the course “Mechanized semantics”, Collège de France, 2019-2020
rocq-community/autosubst - Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
coq-io/io - A library for effects in Coq.
mit-plv/rupicola - Gallina to Bedrock2 compilation toolkit
mit-plv/bedrock - Coq library for verified low-level programming
choukh/Set-Theory - A formalization of the textbook Elements of Set Theory
sigurdschneider/lvc - LVC verified compiler
philzook58/nand2coq - Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
meithecatte/busycoq - Busy Beaver deciders backed by Coq proof
tchajed/iris-simp-lang - We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
anton-trunov/coq-lecture-notes - Coq Lecture Notes (WIP)
rocq-community/semantics - A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
jtassarotti/coq-proba - A Probability Theory Library for the Coq Theorem Prover
geohot/coq-hardy - Formalizing the Theorems from Hardy’s “An Introduction to the Theory of Numbers” in coq
lthms/FreeSpec - A framework for implementing and certifying impure computations in Coq
snu-sf/paco - A Coq library for parametric coinduction
rocq-community/topology - General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
MichaelBurge/pornview - Porn browser formally-verified in Coq
math-comp/finmap - Finite sets, finite maps, multisets and generic sets
uwplse/pumpkin-pi - An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
rocq-community/fav-ssr - Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
mit-plv/coqutil - Coq library for tactics, basic definitions, sets, maps
cmeiklejohn/distributed-data-structures - Distributed Data Structures in Coq
tchajed/coq-record-update - Library to create Coq record update functions
damien-pous/relation-algebra - Relation algebra library for Coq
rocq-community/reglang - Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
foreverbell/verified - Coq formalizations and proofs of (data) structures and algorithms.
wouter-swierstra/xmonad - xmonad in Coq
vrahli/NuprlInCoq - Implementation of Nuprl’s type theory in Coq
tchajed/ltac2-tutorial - Ltac2 tutorial
rocq-community/parseque - Total Parser Combinators in Coq [maintainer=@womeier]
choukh/Baby-Set-Theory - Coq集合论中文教程
CertiCoq/VeriFFI - VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project
arthuraa/poleiro - A blog about Coq
impermeable/coq-waterproof - The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
rocq-community/paramcoq - Old Coq plugin for parametricity [maintainer=@ppedrot]
rocq-community/dedekind-reals - A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
pirapira/evmverif - An EVM code verification framework in Coq
dschepler/coq-sequent-calculus - Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic
snu-sf/promising-coq - The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
thery/coqprime - Prime numbers for Coq
marshall-lee/software_foundations - My solutions to Software Foundations course in Coq proof assistant.
xavierleroy/cdf-program-logics - Companion Coq development for Xavier Leroy’s 2021 lectures on program logics
rocq-community/graph-theory - Graph Theory [maintainers=@chdoc,@damien-pous]
inQWIRE/QuantumLib - Coq library for reasoning about quantum programs
math-comp/Coq-Combi - Algebraic Combinatorics in Coq
charguer/tlc - Library for Classical Coq
vlopezj/coq-course - Coq course at Chalmers CSE
takanuva/cps - A formalization of continuation-passing style calculi in Coq [WIP]
math-comp/algebra-tactics - Ring, field, lra, nra, and psatz tactics for Mathematical Components
formal-land/coq-of-python - Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
fblanqui/color - Coq library on rewriting theory and termination
EasyCrypt/certicrypt - CertiCrypt Coq Framework
math-comp/odd-order - The formal proof of the Odd Order Theorem
Lysxia/system-F - Formalization of the polymorphic lambda calculus and its parametricity theorem
langston-barrett/coq-big-o - A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
gangtan/CPUmodels - GoNative project: formal machines models in Coq
rocq-community/coq-program-verification-template - Template project for program verification in Coq, showcasing reasoning on CompCert’s Clight language using the Verified Software Toolchain [maintainer=@palmskog]
pedrotst/coquedille - A Coq to Cedille compiler written in Coq
logsem/aneris - Program logic for developing and verifying distributed systems
VeriNum/vcfloat - VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
rocq-community/chapar - A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Lysxia/coq-simple-io - IO for Gallina
codyroux/broad-coq-tutorial - Some unstructured notes concerning the Broad tutorial to take place in March 2020
vrahli/Velisarios - A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
rocq-community/gaia - Implementation of books from Bourbaki’s Elements of Mathematics in Coq [maintainer=@thery]
rocq-community/dblib - Coq library for working with de Bruijn indices [maintainer=@KevOrr]
pa-ba/calc-comp - Coq proofs for the paper “Calculating Correct Compilers”
imdea-software/fcsl-pcm - Partial Commutative Monoids
bmsherman/topology - Formal topology (and some probability) in Coq
rocq-community/goedel - Archived since the contents have been moved to the Hydras & Co. repository
reynir/Brainfuck - Brainfuck formalized in Coq
math-comp/Abel - A proof of Abel-Ruffini theorem.
arthuraa/extructures - Finite sets and maps for Coq with extensional equality
acorrenson/SATurne - Tiny verified SAT-solver
weakmemory/imm - Intermediate Memory Model (IMM) and compilation correctness proofs for it
vafeiadis/hahn - Hahn: A Coq library
rafaelcgs10/W-in-Coq - This is a Coq formalization of Damas-Milner type system and its algorithm W.
logsem/clutch - Probabilistic separation logics for verifying higher-order probabilistic programs.
tezos/tezoscoq - working with coq and tezos
math-comp/mczify - Micromega tactics for Mathematical Components
llee454/functional-algebra - This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
formal-land/coq-bonsai - 🌳 Generate a fresh bonsai in your terminal
affeldt-aist/coq-robot - Mathematics of Robotic Manipulation using Rocq and MathComp
rocq-community/lemma-overloading - Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
CoqHott/logrel-coq - Logical Relation for MLTT in Coq
arthuraa/deriving - Class instances for Coq inductive types with little boilerplate
thery/hanoi - Hanoi tower in Coq
rocq-community/trocq - A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx]
novifinancial/LibraChain - A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover
dboulytchev/miniKanren-coq - A certified semantics for relational programming workout.
coq-ext-lib/coq-compile - A compiler for Coq
sweirich/graded-haskell - Graded Dependent Type systems
rocq-community/bignums - Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
rocq-community/apery - A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
rocq-community/alea - Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
pi8027/stablesort - Stable sort algorithms and their stability proofs in Rocq
lastland/ClairvoyanceMonad - The Coq formalization of the paper Reasoning about the garden of forking paths.
AU-COBRA/PoS-NSB - A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq
Zilliqa/scilla-coq - State-Transition Systems for Smart Contracts
uwplse/StructTact - Coq utility and tactic library.
uwplse/cheerios - Formally verified Coq serialization library with support for extraction to OCaml
sudgy/math-from-nothing - Developing mathematics in Coq from the ground up
rocq-community/coqoban - Sokoban (in Coq) [maintainer=@erikmd]
rocq-community/bits - A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
rocq-community/atbr - Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
rocq-archive/zfc - An encoding of Zermelo-Fraenkel Set Theory in Coq
dunnl/tealeaves - A Coq library for abstract syntactical reasoning
Coq-Polyhedra/Coq-Polyhedra - Formalizing convex polyhedra in Coq
rocq-prover/platform-docs - A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
jwiegley/coq-cds4ltl - A formal verification of Linear Temporal Logic in Coq
coq-io/system - Library of Unix effects for Coq.
Yosuke-Ito-345/Actuary - Formalization of the basic actuarial mathematics using Coq
xavierleroy/cdf-sem-meca - Développement Coq pour le cours “Sémantiques mécanisées”, Collège de France, 2019-2020
verif-scop/PolCert - A verified polyhedral scheduling validator in Coq.
thery/T2048 - a version of the 2048 game for Coq
sifive/ProcKami - Kami based processor implementations and specifications
rocq-community/hoare-tut - A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
mgrabovsky/fm-notes - Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
kai-qu/linear-logic - An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
bobatkey/system-f-parametricity-model - A Model of Relationally Parametric System F in Coq
xavierleroy/canonical-binary-tries - Coq development accompanying the paper “Efficient Extensional Binary Tries”
rodrigogribeiro/unification - Formalisation of a type unification algorithm in Coq proof assistant.
rocq-community/HighSchoolGeometry - Geometry in Coq for French high school [maintainer=@thery]
Matafou/LibHyps - A Coq library providing tactics to deal with hypothesis
jwiegley/coq-lattice - A reflection-based proof tactic for lattices in Coq
Huxpro/WasmCert - A (in-development) Coq mechanization of WebAssembly specification.
damien-pous/coinduction - coinduction library for Coq
choukh/CategoryTheory - A Coq formalization of the textbook Categories and Toposes: Visualized and Explained
CertiKOS/coqrel - Binary logical relations library for the Coq proof assistant
aslanix/SmallStepNI - Mechanization of a noninterference proof for a toy imperative language with small-step semantics in Coq
mmcco/verified-parser-example - A minimal example of a formally verified parser using ocamllex and Menhir’s Coq backend.
micro-policies/micro-policies-coq - Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
LLM4Rocq/miniF2F-rocq - A Rocq version of the miniF2F dataset
bluerock-io/BRiCk - Formalization of C++ for verification purposes.
mit-pdos/perennial - Verifying concurrent crash-safe systems
rocq-community/coq-tricks - Tricks you wish the Coq manual told you [maintainer=@tchajed]
affeldt-aist/infotheo - A Coq formalization of information theory and linear error-correcting codes
affeldt-aist/monae - Monadic effects and equational reasoning in Coq
huynhtrankhanh/CoqCP - We combat sloppy arguments in competitive programming and raise the standard of rigor
rocq-community/sudoku - A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
coq-community/coq-tricks - Tricks you wish the Coq manual told you [maintainer=@tchajed]
MetaCoq/metacoq - Metaprogramming, verified meta-theory and implementation of Coq in Coq
coq-community/fourcolor - Formal proof of the Four Color Theorem [maintainer=@ybertot]
coq-community/math-classes - A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
coq-community/coq-ext-lib - A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
coq-community/coq-art - Coq code and exercises from the Coq’Art book [maintainers=@ybertot,@Casteran]
coq-community/corn - Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
coq-community/coq-dpdgraph - Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
coq-community/hydra-battles - Variations on Kirby & Paris’ hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
coq-community/coqeal - The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
coq-community/autosubst - Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
coq-community/topology - General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
coq-community/semantics - A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
coq-community/paramcoq - Old Coq plugin for parametricity [maintainer=@ppedrot]
coq-community/fav-ssr - Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
coq-community/parseque - Total Parser Combinators in Coq [maintainer=@womeier]
coq-community/dedekind-reals - A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
coq-community/reglang - Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
coq-community/graph-theory - Graph Theory [maintainers=@chdoc,@damien-pous]
coq-community/chapar - A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
coq-community/coq-program-verification-template - Template project for program verification in Coq, showcasing reasoning on CompCert’s Clight language using the Verified Software Toolchain [maintainer=@palmskog]
coq-community/gaia - Implementation of books from Bourbaki’s Elements of Mathematics in Coq [maintainer=@thery]
coq-community/dblib - Coq library for working with de Bruijn indices [maintainer=@KevOrr]
coq-community/goedel - Archived since the contents have been moved to the Hydras & Co. repository
coq-community/lemma-overloading - Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
coq-community/alea - Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
coq-community/atbr - Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
coq-community/bits - A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
coq-community/bignums - Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
coq/platform-docs - A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
coq-community/coqoban - Sokoban (in Coq) [maintainer=@erikmd]
coq-community/trocq - A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
coq-community/sudoku - A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
coq-community/HighSchoolGeometry - Geometry in Coq for French high school [maintainer=@thery]
coq-community/apery - A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
bedrocksystems/BRiCk - Formalization of C++ for verification purposes.
ejgallego/coq-serapi - Coq Protocol Playground with Se(xp)rialization of Internal Structures.
coq-contribs/coq-in-coq - A formalisation of the Calculus of Constructions
coq-contribs/zfc - An encoding of Zermelo-Fraenkel Set Theory in Coq
tchajed/coq-tricks - Tricks you wish the Coq manual told you
andrejbauer/dedekind-reals - A formalization of the Dedekind reals in Coq
vellvm/vellvm - The Vellvm (Verified LLVM) coq development.
gallais/parseque - Total Parser Combinators in Coq
palmskog/coq-program-verification-template - Template project for program verification in Coq
Blaisorblade/dot-iris - Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
LogicalAtomist/principia - The Principia Rewrite
certichain/toychain - A minimalistic blockchain consensus implemented and verified in Coq
coq-community/coq-100-theorems - Statements of famous theorems proven in Coq [maintainer=@jmadiot]
smtcoq/smtcoq - Communication between Coq and SAT/SMT solvers
smorimoto/coq-to-ocaml-to-js - Proof of concept to generate safe and fast JavaScript
certichain/ceramist - Verified hash-based AMQ structures in Coq
math-comp/fourcolor - Formal proof of the Four Color Theorem
foobar-land/coq-bonsai - 🌳 Generate a fresh bonsai in your terminal
bedrocksystems/cpp2v - Formalization of C++ for verification purposes.
hivert/Coq-Combi - Algebraic Combinatorics in Coq
Karmaki/coq-dpdgraph - Build dependency graphs between COQ objects
CoqEAL/CoqEAL - CoqEAL — The Coq Effective Algebra Library
heades/System-F-Coq - System F in coq.
project-oak/oak-hardware - Formal specification and verification of hardware, especially for security and privacy.
coq-community/coq100 - Statements of famous theorems proven in Coq [maintainer=@jmadiot]
ANSSI-FR/FreeSpec - A framework for implementing and certifying impure computations in Coq
uds-psl/autosubst - Automation for de Bruijn syntax and substitution in Coq
uwplse/ornamental-search - DEVOID: Ornaments for Proof Reuse in Coq
coq-ext-lib/coq-ext-lib - A library of Coq definitions, theorems, and tactics.
siddharthist/coq-big-o - A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
hazelgrove/hazel - Hazel, a live functional programming environment with typed holes
Template-Coq/template-coq - Reflection library for Coq
math-classes/math-classes - A library of abstract interfaces for mathematical structures in Coq.
c-corn/corn - Coq Repository at Nijmegen
stepchowfun/coq-fun - A selection of Coq developments.
uwdb/Cosette - Cosette is an automated SQL solver powered by Coq and Rosette.
DDCSF/iron - Coq formalizations of functional languages.
vladimirias/Foundations - Development of the univalent foundations of mathematics in Coq
aspiwack/cosa - Coq-verified Shape Analysis
Ptival/HaysTac - A pile of Ltac tactics that might contain the needle you’re looking for. Oriented around nameless tactics programming.
EugeneLoy/coq_jupyter - Jupyter Notebook kernel for Coq