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
• UniMath/UniMath - This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
• formal-land/coq-of-rust - Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦
• 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/coq-tricks - Tricks you wish the Coq manual told you [maintainer=@tchajed]
• PrincetonUniversity/VST - Verified Software Toolchain
• MetaRocq/metarocq - Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
• princeton-vl/CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant
• stepchowfun/proofs - My personal repository of formally verified mathematics.
• jasmin-lang/jasmin - Language for high-assurance and high-speed cryptography
• antalsz/hs-to-coq - Convert Haskell source code to Coq source code
• QuickChick/QuickChick - Randomized Property-Based Testing Plugin for Coq
• UniMath/Foundations - Voevodsky's original development of the univalent foundations of mathematics in Coq
• mit-pdos/fscq - FSCQ is a certified file system written and proven in Coq
• mattam82/Coq-Equations - A function definition package for Coq
• math-comp/analysis - Mathematical Components compliant Analysis Library
• DeepSpec/InteractionTrees - A Library for Representing Recursive and Impure Programs in Coq
• 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
• mit-pdos/perennial - Verifying concurrent crash-safe systems
• barry-jay-personal/tree-calculus - Proofs in Coq for the book Reflective Programs in Tree Calculus
• 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]
• LPCIC/coq-elpi - Coq plugin embedding elpi
• ilyasergey/pnp - Lecture notes for a short course on proving/programming in Coq via SSReflect.
• 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
• mit-plv/koika - A core language for rule-based hardware design 🦑
• 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.
• project-oak/silveroak - Formal specification and verification of hardware, especially for security and privacy.
• verse-lab/ceramist - Verified hash-based AMQ structures in Coq
• rocq-community/coq-art - Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
• AU-COBRA/ConCert - A framework for smart contract verification in Coq
• uds-psl/coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
• rocq-community/corn - Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
• mit-plv/riscv-coq - RISC-V Specification in Coq
• verse-lab/toychain - A minimalistic blockchain consensus implemented and verified in Coq
• Ptival/PeaCoq - PeaCoq is a pretty Coq, isn't it?
• WasmCert/WasmCert-Coq - A mechanisation of Wasm in Coq(Rocq)
• DistributedComponents/disel - Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
• sec-bit/tokenlibs-with-proofs - Correctness proofs of Ethereum token contracts
• math-comp/hierarchy-builder - High level commands to declare a hierarchy based on packed classes
• clarus/falso - A proof of false in Coq.
• amintimany/Categories - A formalization of category theory in the Coq proof assistant.
• 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]
• coq-concurrency/pluto - A web server written in Coq.
• inQWIRE/SQIR - A Small Quantum Intermediate Representation
• plclub/hs-to-coq - Convert Haskell source code to Coq source code.
• pi8027/lambda-calculus - A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
• bluerock-io/BRiCk - Formalization of C++ for verification purposes.
• rocq-community/hydra-battles - Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
• imdea-software/htt - Hoare Type Theory
• ml4tp/gamepad - A Learning Environment for Theorem Proving
• rocq-community/coqeal - The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
• affeldt-aist/monae - Monadic effects and equational reasonig in Coq
• affeldt-aist/infotheo - A Coq formalization of information theory and linear error-correcting codes
• rocq-archive/coq-in-coq - A formalisation of the Calculus of Constructions
• INRIA/velus - A Lustre compiler in Coq
• xavierleroy/cdf-mech-sem - Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
• SSProve/ssprove - A foundational framework for modular cryptographic proofs in Coq
• coq-io/io - A library for effects in Coq.
• mit-plv/bedrock - Coq library for verified low-level programming
• choukh/Set-Theory - A formalization of the textbook Elements of Set Theory
• rocq-community/autosubst - Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
• 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).
• 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
• anton-trunov/coq-lecture-notes - Coq Lecture Notes (WIP)
• mit-plv/rupicola - Gallina to Bedrock2 compilation toolkit
• lthms/FreeSpec - A framework for implementing and certifying impure computations in Coq
• MichaelBurge/pornview - Porn browser formally-verified in Coq
• 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.
• uwplse/pumpkin-pi - An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
• meithecatte/busycoq - Busy Beaver deciders backed by Coq proof
• cmeiklejohn/distributed-data-structures - Distributed Data Structures in Coq
• 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]
• damien-pous/relation-algebra - Relation algebra library for Coq
• snu-sf/paco - A Coq library for parametric coinduction
• rocq-community/topology - General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
• rocq-community/fav-ssr - Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
• mit-plv/coqutil - Coq library for tactics, basic definitions, sets, maps
• math-comp/finmap - Finite sets, finite maps, multisets and generic sets
• foreverbell/verified - Coq formalizations and proofs of (data) structures and algorithms.
• arthuraa/poleiro - A blog about Coq
• wouter-swierstra/xmonad - xmonad in Coq
• vrahli/NuprlInCoq - Implementation of Nuprl's type theory in Coq
• tchajed/ltac2-tutorial - Ltac2 tutorial
• tchajed/coq-record-update - Library to create Coq record update functions
• rocq-community/paramcoq - Old Coq plugin for parametricity [maintainer=@ppedrot]
• 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
• 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
• rocq-community/parseque - Total Parser Combinators in Coq [maintainer=@womeier]
• rocq-community/dedekind-reals - A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
• rocq-community/reglang - Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
• xavierleroy/cdf-program-logics - Companion Coq development for Xavier Leroy's 2021 lectures on program logics
• inQWIRE/QuantumLib - Coq library for reasoning about quantum programs
• charguer/tlc - Library for Classical Coq
• vlopezj/coq-course - Coq course at Chalmers CSE
• math-comp/Coq-Combi - Algebraic Combinatorics in Coq
• thery/coqprime - Prime numbers for Coq
• takanuva/cps - A formalization of continuation-passing style calculi in Coq [WIP]
• snu-sf/promising-coq - The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
• marshall-lee/software_foundations - My solutions to Software Foundations course in Coq proof assistant.
• 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.
• gangtan/CPUmodels - GoNative project: formal machines models in Coq
• fblanqui/color - Coq library on rewriting theory and termination
• rocq-community/graph-theory - Graph Theory [maintainers=@chdoc,@damien-pous]
• langston-barrett/coq-big-o - A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
• EasyCrypt/certicrypt - CertiCrypt Coq Framework
• Lysxia/system-F - Formalization of the polymorphic lambda calculus and its parametricity theorem
• logsem/aneris - Program logic for developing and verifying distributed systems
• formal-land/coq-of-python - Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
• pedrotst/coquedille - A Coq to Cedille compiler written in Coq
• math-comp/algebra-tactics - Ring, field, lra, nra, and psatz tactics for Mathematical Components
• 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
• bmsherman/topology - Formal topology (and some probability) in Coq
• vrahli/Velisarios - A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
• 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]
• codyroux/broad-coq-tutorial - Some unstructured notes concerning the Broad tutorial to take place in March 2020
• vafeiadis/hahn - Hahn: A Coq library
• 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"
• math-comp/odd-order - The formal proof of the Odd Order Theorem
• arthuraa/extructures - Finite sets and maps for Coq with extensional equality
• rocq-community/goedel - Archived since the contents have been moved to the Hydras & Co. repository
• rafaelcgs10/W-in-Coq - This is a Coq formalization of Damas-Milner type system and its algorithm W.
• math-comp/Abel - A proof of Abel-Ruffini theorem.
• VeriNum/vcfloat - VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
• tezos/tezoscoq - working with coq and tezos
• 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.
• imdea-software/fcsl-pcm - Partial Commutative Monoids
• rocq-community/lemma-overloading - Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
• acorrenson/SATurne - Tiny verified SAT-solver
• weakmemory/imm - Intermediate Memory Model (IMM) and compilation correctness proofs for it
• reynir/Brainfuck - Brainfuck formalized in Coq
• 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
• affeldt-aist/coq-robot - Mathematics of Rigid Body Transformationss using Coq and MathComp
• thery/hanoi - Hanoi tower in Coq
• rocq-community/alea - Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
• math-comp/mczify - Micromega tactics for Mathematical Components
• 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.
• sweirich/graded-haskell - Graded Dependent Type systems
• lastland/ClairvoyanceMonad - The Coq formalization of the paper Reasoning about the garden of forking paths.
• formal-land/coq-bonsai - 🌳 Generate a fresh bonsai in your terminal
• Coq-Polyhedra/Coq-Polyhedra - Formalizing convex polyhedra in Coq
• CoqHott/logrel-coq - Logical Relation for MLTT in Coq
• arthuraa/deriving - Class instances for Coq inductive types with little boilerplate
• uwplse/cheerios - Formally verified Coq serialization library with support for extraction to OCaml
• 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-community/apery - A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
• rocq-archive/zfc - An encoding of Zermelo-Fraenkel Set Theory in Coq
• logsem/clutch - Probabilistic separation logics for verifying higher-order probabilistic programs.
• dunnl/tealeaves - A Coq library for abstract syntactical reasoning
• coq-io/system - Library of Unix effects for Coq.
• xavierleroy/canonical-binary-tries - Coq development accompanying the paper "Efficient Extensional Binary Tries"
• thery/T2048 - a version of the 2048 game for Coq
• sifive/ProcKami - Kami based processor implementations and specifications
• rocq-community/coqoban - Sokoban (in Coq) [maintainer=@erikmd]
• 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]
• pi8027/stablesort - Stable sort algorithms and their stability proofs in Coq
• mgrabovsky/fm-notes - Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
• bobatkey/system-f-parametricity-model - A Model of Relationally Parametric System F in 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
• Matafou/LibHyps - A Coq library providing tactics to deal with hypothesis
• kai-qu/linear-logic - An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
• jwiegley/coq-lattice - A reflection-based proof tactic for lattices in Coq
• Huxpro/WasmCert - A (in-development) Coq mechanization of WebAssembly specification.
• CertiKOS/coqrel - Binary logical relations library for the Coq proof assistant
• verif-scop/PolCert - A verified polyhedral scheduling validator in Coq.
• sudgy/math-from-nothing - Developing mathematics in Coq from the ground up
• rocq-prover/platform-docs - A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
• rocq-community/trocq - A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
• rocq-community/hoare-tut - A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
• rocq-community/HighSchoolGeometry - Geometry in Coq for French high school [maintainer=@thery]
• 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
• jwiegley/coq-cds4ltl - A formalization of finite, constructive log analysis using linear temporal logic
• choukh/CategoryTheory - A Coq formalization of the textbook Categories and Toposes: Visualized and Explained
• 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