A curated list of awesome Coq frameworks, libraries and software.
- AbsInt/CompCert - The CompCert formally-verified C compiler
- UniMath/UniMath - This coq 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
- uwplse/verdi - A framework for formally verifying distributed systems implementations in Coq
- math-comp/math-comp - Mathematical Components
- tchajed/coq-tricks - Tricks you wish the Coq manual told you
- PrincetonUniversity/VST - Verified Software Toolchain
- vellvm/vellvm - The Vellvm (Verified LLVM) coq development.
- princeton-vl/CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant
- antalsz/hs-to-coq - Convert Haskell source code to Coq source code
- MetaCoq/metacoq - Metaprogramming in Coq
- stepchowfun/proofs - My personal repository of formally verified mathematics.
- UniMath/Foundations - Voevodsky's original development of the univalent foundations of mathematics in Coq
- QuickChick/QuickChick - Randomized Property-Based Testing Plugin for Coq
- mit-pdos/fscq - FSCQ is a certified file system written and proven in Coq
- jscert/jscert - A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
- mattam82/Coq-Equations - A function definition package for Coq
- LogicalAtomist/principia - The Principia Rewrite
- 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
- clarus/coq-chick-blog - 🐣 A blog engine written and proven in Coq
- uwplse/verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
- DeepSpec/InteractionTrees - A Library for Representing Recursive and Impure Programs in Coq
- jwiegley/coq-haskell - A library for formalizing Haskell types and functions in Coq
- coq-community/math-classes - A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
- GeoCoq/GeoCoq - A formalization of geometry in Coq based on Tarski's axiom system
- Lysxia/advent-of-coq-2018 - Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
- math-comp/analysis - Mathematical Components compliant Analysis Library
- ilyasergey/pnp - Lecture notes for a short course on proving/programming in Coq via SSReflect.
- discus-lang/iron - Coq formalizations of functional languages.
- coq-community/fourcolor - Formal proof of the Four Color Theorem [maintainer=@ybertot]
- mit-plv/kami - A Platform for High-Level Parametric Hardware Specification and its Modular Verification
- verse-lab/ceramist - Verified hash-based AMQ structures in Coq
- jasmin-lang/jasmin - Jasmin compiler
- coq-community/coq-ext-lib - A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
- Ptival/PeaCoq - PeaCoq is a pretty Coq, isn't it?
- coq-community/corn - Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]
- project-oak/silveroak - Formal specification and verification of hardware, especially for security and privacy.
- certichain/toychain - A minimalistic blockchain consensus implemented and verified in Coq
- CertiCoq/certicoq - A Verified Compiler for Gallina, Written in Gallina
- mit-plv/koika - A core language for rule-based hardware design 🦑
- sec-bit/tokenlibs-with-proofs - Correctness proofs of Ethereum token contracts
- amintimany/Categories - A formalization of category theory in the Coq proof assistant.
- DistributedComponents/disel - Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
- mit-pdos/perennial - Verifying concurrent crash-safe systems
- coq-concurrency/pluto - A web server written in Coq.
- uds-psl/coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
- clarus/falso - A proof of false in Coq.
- mit-plv/riscv-coq - RISC-V Specification in Coq
- coq-community/coq-dpdgraph - Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
- AU-COBRA/ConCert - A framework for smart contract verification in Coq
- pi8027/lambda-calculus - A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
- coq-community/coq-art - Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
- ymherklotz/vericert - A formally verified high-level synthesis tool based on CompCert and written in Coq.
- ml4tp/gamepad - A Learning Environment for Theorem Proving
- plclub/hs-to-coq - Convert Haskell source code to Coq source code.
- coq-io/io - A library for effects in Coq.
- affeldt-aist/monae - Monadic effects and equational reasonig in Coq
- WasmCert/WasmCert-Coq - A mechanisation of Wasm in Coq
- coq-community/coqeal - The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
- inQWIRE/SQIR - A Small Quantum Intermediate Representation
- affeldt-aist/infotheo - A Coq formalization of information theory and linear error-correcting codes
- imdea-software/htt - Hoare Type Theory
- choukh/Set-Theory - A formalization of the textbook Elements of Set Theory
- sigurdschneider/lvc - LVC verified compiler
- coq-contribs/coq-in-coq - A formalisation of the Calculus of Constructions
- lthms/FreeSpec - A framework for implementing and certifying impure computations in Coq
- bedrocksystems/BRiCk - Formalization of C++ for verification purposes.
- geohot/coq-hardy - Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
- philzook58/nand2coq - Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
- INRIA/velus - A Lustre compiler in Coq
- cmeiklejohn/distributed-data-structures - Distributed Data Structures in Coq
- anton-trunov/coq-lecture-notes - Coq Lecture Notes (WIP)
- MichaelBurge/pornview - Porn browser formally-verified in Coq
- math-comp/finmap - Finite sets, finite maps, multisets and generic sets
- arthuraa/poleiro - A blog about Coq
- wouter-swierstra/xmonad - xmonad in Coq
- pirapira/evmverif - An EVM code verification framework in Coq
- jtassarotti/coq-proba - A Probability Theory Library for the Coq Theorem Prover
- coq-community/paramcoq - Coq plugin for parametricity [maintainer=@proux01]
- uwplse/pumpkin-pi - An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
- coq-community/autosubst - Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
- mit-plv/rupicola - Gallina to Bedrock2 compilation toolkit
- foreverbell/verified - Coq formalizations and proofs of (data) structures and algorithms.
- dschepler/coq-sequent-calculus - Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic
- mit-plv/bedrock - Coq library for verified low-level programming
- coq-community/topology - General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
- xavierleroy/cdf-mech-sem - Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
- vrahli/NuprlInCoq - Implementation of Nuprl's type theory in Coq
- tchajed/coq-record-update - Library to create Coq record update functions
- andrejbauer/dedekind-reals - A formalization of the Dedekind reals in Coq
- gallais/parseque - Total Parser Combinators in Coq
- damien-pous/relation-algebra - Relation algebra library for Coq
- coq-community/coq-100-theorems - Statements of famous theorems proven in Coq [maintainer=@jmadiot]
- 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.
- coq-community/hydra-battles - Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
- snu-sf/paco - A Coq library for parametric coinduction
- mit-plv/coqutil - Coq library for tactics, basic definitions, sets, maps
- vlopezj/coq-course - Coq course at Chalmers CSE
- tchajed/ltac2-tutorial - Ltac2 tutorial
- snu-sf/promising-coq - The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
- langston-barrett/coq-big-o - A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
- choukh/Baby-Set-Theory - Coq集合论中文教程
- bmsherman/topology - Formal topology (and some probability) in Coq
- barry-jay-personal/tree-calculus - Proofs in Coq for the book Reflective Programs in Tree Calculus
- SSProve/ssprove - A foundational framework for modular cryptographic proofs in Coq
- math-comp/Coq-Combi - Algebraic Combinatorics in Coq
- coq-community/reglang - Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
- coq-community/chapar - A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
- tezos/tezoscoq - working with coq and tezos
- vafeiadis/hahn - Hahn: A Coq library
- rafaelcgs10/W-in-Coq - This is a Coq formalization of Damas-Milner type system and its algorithm W.
- pedrotst/coquedille - A Coq to Cedille compiler written in Coq
- pa-ba/calc-comp - Coq proofs for the paper "Calculating Correct Compilers"
- math-comp/Abel - A proof of Abel-Ruffini theorem.
- fblanqui/color - Coq library on rewriting theory and termination
- 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]
- xavierleroy/cdf-program-logics - Companion Coq development for Xavier Leroy's 2021 lectures on program logics
- palmskog/coq-program-verification-template - Template project for program verification in Coq
- gangtan/CPUmodels - GoNative project: formal machines models in Coq
- coq-ext-lib/coq-compile - A compiler for Coq
- coq-community/goedel - Archived since the contents have been moved to the Hydras & Co. repository
- coq-community/dblib - Coq library for working with de Bruijn indices [maintainer=@KevOrr]
- codyroux/broad-coq-tutorial - Some unstructured notes concerning the Broad tutorial to take place in March 2020
- charguer/tlc - Library for Classical Coq
- math-comp/algebra-tactics - Ring and field tactics for Mathematical Components
- coq-community/graph-theory - Graph Theory [maintainers=@chdoc,@damien-pous]
- Blaisorblade/dot-iris - Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
- arthuraa/extructures - Finite sets and maps for Coq with extensional equality
- affeldt-aist/coq-robot - Mathematics of Rigid Body Transformationss using Coq and MathComp
- Lysxia/coq-simple-io - IO for Gallina
- coq-community/lemma-overloading - Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
- thery/coqprime - Prime numbers for Coq
- sifive/ProcKami - Kami based processor implementations and specifications
- 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.
- Zilliqa/scilla-coq - State-Transition Systems for Smart Contracts
- vrahli/Velisarios - A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
- uwplse/StructTact - Coq utility and tactic library.
- reynir/Brainfuck - Brainfuck formalized in Coq
- novifinancial/LibraChain - A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover
- EasyCrypt/certicrypt - CertiCrypt Coq Framework
- coq-io/system - Library of Unix effects for 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
- thery/T2048 - a version of the 2048 game for Coq
- math-comp/odd-order - The formal proof of the Odd Order Theorem
- logsem/aneris - Program logic for developing and verifying distributed systems
- imdea-software/fcsl-pcm - Partial Commutative Monoids
- coq-community/gaia - Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
- coq-community/atbr - Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
- coq-community/alea - Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
- bobatkey/system-f-parametricity-model - A Model of Relationally Parametric System F in Coq
- sweirich/graded-haskell - Graded Dependent Type systems
- Huxpro/WasmCert - A (in-development) Coq mechanization of WebAssembly specification.
- formal-land/coq-bonsai - 🌳 Generate a fresh bonsai in your terminal
- 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]
- smtcoq/smtcoq - Communication between Coq and SAT/SMT solvers
- smorimoto/coq-to-ocaml-to-js - Proof of concept to generate safe and fast JavaScript
- dboulytchev/miniKanren-coq - A certified semantics for relational programming workout.
- 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
- Lysxia/system-F - Formalization of the polymorphic lambda calculus and its parametricity theorem
- 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.
- math-comp/hierarchy-builder - High level commands to declare a hierarchy based on packed classes
- 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
- LPCIC/coq-elpi - Coq plugin embedding elpi
- 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