awesome-coq

Coq libraries and frameworks

A curated collection of verified and useful libraries and frameworks for the Coq proof assistant.

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

GitHub
236 stars
22 watching
16 forks
last commit: 2 days ago
Linked from 1 awesome list


awesome-coq
AbsInt/CompCert 1,888 22 days ago The CompCert formally-verified C compiler
HoTT/Coq-HoTT 1,252 14 days ago A Coq library for Homotopy Type Theory
UniMath/UniMath 961 9 days ago This coq library aims to formalize a substantial body of mathematics using the univalent point of view
magmide/magmide 812 8 months ago A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers
jwiegley/category-theory 754 about 2 months ago An axiom-free formalization of category theory in Coq for personal study and practical work
uwplse/verdi 589 6 months ago A framework for formally verifying distributed systems implementations in Coq
math-comp/math-comp 587 6 days ago Mathematical Components
coq-community/coq-tricks 503 3 months ago Tricks you wish the Coq manual told you [maintainer=@tchajed]
PrincetonUniversity/VST 442 9 days ago Verified Software Toolchain
formal-land/coq-of-rust 421 6 days ago Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
princeton-vl/CoqGym 384 over 1 year ago A Learning Environment for Theorem Proving with the Coq proof assistant
MetaCoq/metacoq 382 5 days ago Metaprogramming, verified meta-theory and implementation of Coq in Coq
stepchowfun/proofs 291 24 days ago My personal repository of formally verified mathematics
antalsz/hs-to-coq 279 about 4 years ago Convert Haskell source code to Coq source code
jasmin-lang/jasmin 269 5 days ago Language for high-assurance and high-speed cryptography
QuickChick/QuickChick 254 20 days ago Randomized Property-Based Testing Plugin for Coq
UniMath/Foundations 240 about 10 years ago Voevodsky's original development of the univalent foundations of mathematics in Coq
mit-pdos/fscq 236 about 2 years ago FSCQ is a certified file system written and proven in Coq
mattam82/Coq-Equations 223 9 days ago A function definition package for Coq
math-comp/analysis 206 6 days ago Mathematical Components compliant Analysis Library
DeepSpec/InteractionTrees 203 about 1 month ago A Library for Representing Recursive and Impure Programs in Coq
sifive/Kami 197 about 4 years ago 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 196 10 months ago A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
GeoCoq/GeoCoq 186 6 months ago A formalization of geometry in Coq based on Tarski's axiom system
uwplse/verdi-raft 183 12 months ago An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
clarus/coq-chick-blog 178 almost 5 years ago 🐣 A blog engine written and proven in Coq
jwiegley/coq-haskell 167 about 1 year ago A library for formalizing Haskell types and functions in Coq
coq-community/fourcolor 166 7 days ago Formal proof of the Four Color Theorem [maintainer=@ybertot]
mit-pdos/perennial 163 3 days ago Verifying concurrent crash-safe systems
coq-community/math-classes 162 18 days ago A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
ilyasergey/pnp 160 over 3 years ago Lecture notes for a short course on proving/programming in Coq via SSReflect
mit-plv/kami 142 about 2 months ago A Platform for High-Level Parametric Hardware Specification and its Modular Verification
discus-lang/iron 141 over 4 years ago Coq formalizations of functional languages
mit-plv/koika 140 about 1 month ago A core language for rule-based hardware design 🦑
Lysxia/advent-of-coq-2018 140 almost 6 years ago Advent of Code 2018, in Coq! ( )
LPCIC/coq-elpi 139 6 days ago Coq plugin embedding elpi
CertiCoq/certicoq 136 3 months ago A Verified Compiler for Gallina, Written in Gallina
coq-community/coq-ext-lib 129 2 months ago A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
rocq-archive/coq-serapi 128 8 days ago Coq Protocol Playground with Se(xp)rialization of Internal Structures
project-oak/silveroak 124 over 2 years ago Formal specification and verification of hardware, especially for security and privacy
verse-lab/ceramist 121 over 4 years ago Verified hash-based AMQ structures in Coq
AU-COBRA/ConCert 114 6 days ago A framework for smart contract verification in Coq
verse-lab/toychain 111 over 4 years ago A minimalistic blockchain consensus implemented and verified in Coq
uds-psl/coq-library-undecidability 111 about 2 months ago A library of mechanised undecidability proofs in the Coq proof assistant
coq-community/corn 111 8 days ago Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
coq-community/coq-art 110 4 months ago Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
mit-plv/riscv-coq 109 4 months ago RISC-V Specification in Coq
Ptival/PeaCoq 106 over 3 years ago PeaCoq is a pretty Coq, isn't it?
sec-bit/tokenlibs-with-proofs 98 over 5 years ago Correctness proofs of Ethereum token contracts
WasmCert/WasmCert-Coq 95 14 days ago A mechanisation of Wasm in Coq
DistributedComponents/disel 95 4 months ago Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
clarus/falso 93 about 5 years ago A proof of false in Coq
amintimany/Categories 93 17 days ago A formalization of category theory in the Coq proof assistant
ymherklotz/vericert 88 5 months ago A formally verified high-level synthesis tool based on CompCert and written in Coq
coq-concurrency/pluto 86 over 8 years ago A web server written in Coq
coq-community/coq-dpdgraph 86 8 days ago Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
inQWIRE/SQIR 79 3 months ago A Small Quantum Intermediate Representation
plclub/hs-to-coq 78 3 months ago Convert Haskell source code to Coq source code
pi8027/lambda-calculus 78 over 4 years ago A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
ml4tp/gamepad 72 over 2 years ago A Learning Environment for Theorem Proving
imdea-software/htt 69 about 1 month ago Hoare Type Theory
bedrocksystems/BRiCk 69 9 days ago Formalization of C++ for verification purposes
coq-community/hydra-battles 68 9 months ago Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
affeldt-aist/monae 68 27 days ago Monadic effects and equational reasonig in Coq
rocq-archive/coq-in-coq 66 4 months ago A formalisation of the Calculus of Constructions
coq-community/coqeal 66 3 months ago The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
xavierleroy/cdf-mech-sem 64 8 months ago Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
coq-io/io 64 over 2 years ago A library for effects in Coq
affeldt-aist/infotheo 64 7 days ago A Coq formalization of information theory and linear error-correcting codes
INRIA/velus 58 about 1 year ago A Lustre compiler in Coq
choukh/Set-Theory 59 about 3 years ago A formalization of the textbook Elements of Set Theory
sigurdschneider/lvc 57 about 6 years ago LVC verified compiler
mit-plv/bedrock 57 over 7 years ago Coq library for verified low-level programming
SSProve/ssprove 56 20 days ago A foundational framework for modular cryptographic proofs in Coq
philzook58/nand2coq 54 almost 3 years ago Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools)
geohot/coq-hardy 53 over 5 years ago Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
lthms/FreeSpec 52 10 months ago A framework for implementing and certifying impure computations in Coq
coq-community/autosubst 52 2 months ago Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
MichaelBurge/pornview 51 about 7 years ago Porn browser formally-verified in Coq
barry-jay-personal/tree-calculus 51 over 3 years ago Proofs in Coq for the book Reflective Programs in Tree Calculus
mit-plv/rupicola 50 about 2 months ago Gallina to Bedrock2 compilation toolkit
anton-trunov/coq-lecture-notes 50 about 4 years ago Coq Lecture Notes (WIP)
uwplse/pumpkin-pi 49 2 months ago An extension to PUMPKIN PATCH with support for proof repair across type equivalences
tchajed/iris-simp-lang 49 6 months ago We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic
jtassarotti/coq-proba 49 about 1 year ago A Probability Theory Library for the Coq Theorem Prover
cmeiklejohn/distributed-data-structures 49 about 11 years ago Distributed Data Structures in Coq
damien-pous/relation-algebra 48 8 days ago Relation algebra library for Coq
coq-community/topology 47 about 1 month ago General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
arthuraa/poleiro 47 over 2 years ago A blog about Coq
math-comp/finmap 46 6 months ago Finite sets, finite maps, multisets and generic sets
foreverbell/verified 46 over 6 years ago Coq formalizations and proofs of (data) structures and algorithms
coq-community/semantics 45 almost 3 years ago A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
coq-community/fav-ssr 45 7 days ago Functional Algorithms Verified in SSReflect [maintainer=@clayrat]
vrahli/NuprlInCoq 44 almost 4 years ago Implementation of Nuprl's type theory in Coq
pirapira/evmverif 44 about 8 years ago An EVM code verification framework in Coq
dschepler/coq-sequent-calculus 44 over 8 years ago Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic
coq-community/paramcoq 44 2 months ago Coq plugin for parametricity [maintainer=@proux01]
wouter-swierstra/xmonad 43 over 12 years ago xmonad in Coq
snu-sf/paco 43 about 1 month ago A Coq library for parametric coinduction
coq-community/dedekind-reals 43 4 months ago A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
choukh/Baby-Set-Theory 43 almost 3 years ago Coq集合论中文教程
tchajed/ltac2-tutorial 42 about 2 years ago Ltac2 tutorial
tchajed/coq-record-update 42 3 months ago Library to create Coq record update functions
coq-community/parseque 42 11 months ago Total Parser Combinators in Coq [maintainer=@womeier]
mit-plv/coqutil 41 9 days ago Coq library for tactics, basic definitions, sets, maps
coq-community/reglang 41 4 months ago Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
xavierleroy/cdf-program-logics 40 over 3 years ago Companion Coq development for Xavier Leroy's 2021 lectures on program logics
meithecatte/busycoq 39 4 months ago Busy Beaver deciders backed by Coq proof
vlopezj/coq-course 38 over 7 years ago Coq course at Chalmers CSE
charguer/tlc 38 22 days ago Library for Classical Coq
CertiCoq/VeriFFI 35 4 months ago VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project
thery/coqprime 37 15 days ago Prime numbers for Coq
takanuva/cps 36 3 days ago A formalization of continuation-passing style calculi in Coq [WIP]
math-comp/Coq-Combi 36 about 2 months ago Algebraic Combinatorics in Coq
gangtan/CPUmodels 36 over 7 years ago GoNative project: formal machines models in Coq
langston-barrett/coq-big-o 35 over 7 years ago A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces
fblanqui/color 35 18 days ago Coq library on rewriting theory and termination
coq-community/graph-theory 34 4 months ago Graph Theory [maintainers=@chdoc,@damien-pous]
snu-sf/promising-coq 33 about 1 month ago The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
pedrotst/coquedille 33 about 4 years ago A Coq to Cedille compiler written in Coq
Lysxia/system-F 33 over 5 years ago Formalization of the polymorphic lambda calculus and its parametricity theorem
logsem/aneris 33 4 days ago Program logic for developing and verifying distributed systems
impermeable/coq-waterproof 33 8 days ago 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
EasyCrypt/certicrypt 33 over 8 years ago CertiCrypt Coq Framework
math-comp/algebra-tactics 32 2 months ago Ring, field, lra, nra, and psatz tactics for Mathematical Components
marshall-lee/software_foundations 32 5 months ago My solutions to Software Foundations course in Coq proof assistant
inQWIRE/QuantumLib 32 13 days ago Coq library for reasoning about quantum programs
coq-community/chapar 32 11 months ago A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
bmsherman/topology 32 almost 6 years ago Formal topology (and some probability) in Coq
Lysxia/coq-simple-io 31 2 months ago IO for Gallina
codyroux/broad-coq-tutorial 31 about 3 years ago Some unstructured notes concerning the Broad tutorial to take place in March 2020
vafeiadis/hahn 30 5 months ago Hahn: A Coq library
pa-ba/calc-comp 30 12 months ago Coq proofs for the paper "Calculating Correct Compilers"
formal-land/coq-of-python 30 2 months ago Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python
coq-community/dblib 30 about 3 years ago Coq library for working with de Bruijn indices [maintainer=@KevOrr]
coq-community/coq-program-verification-template 29 4 months ago Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
arthuraa/extructures 29 about 1 year ago Finite sets and maps for Coq with extensional equality
vrahli/Velisarios 28 over 5 years ago A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
tezos/tezoscoq 28 over 7 years ago working with coq and tezos
math-comp/Abel 28 6 days ago A proof of Abel-Ruffini theorem
llee454/functional-algebra 28 over 5 years ago 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
coq-community/goedel 28 about 2 years ago Archived since the contents have been moved to the Hydras & Co. repository
coq-community/gaia 28 3 months ago Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
acorrenson/SATurne 28 almost 3 years ago Tiny verified SAT-solver
reynir/Brainfuck 26 over 2 years ago Brainfuck formalized in Coq
imdea-software/fcsl-pcm 26 20 days ago Partial Commutative Monoids
dboulytchev/miniKanren-coq 26 about 4 years ago A certified semantics for relational programming workout
coq-ext-lib/coq-compile 26 over 11 years ago A compiler for Coq
coq-community/lemma-overloading 26 8 days ago Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
affeldt-aist/coq-robot 26 6 months ago Mathematics of Rigid Body Transformationss using Coq and MathComp
rafaelcgs10/W-in-Coq 25 over 4 years ago This is a Coq formalization of Damas-Milner type system and its algorithm W
novifinancial/LibraChain 25 over 4 years ago A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover
math-comp/odd-order 25 22 days ago The formal proof of the Odd Order Theorem
coq-community/alea 25 about 3 years ago Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
AU-COBRA/PoS-NSB 25 almost 4 years ago A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq
Zilliqa/scilla-coq 24 about 4 years ago State-Transition Systems for Smart Contracts
VeriNum/vcfloat 24 4 months ago VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
thery/hanoi 24 about 1 year ago Hanoi tower in Coq
lastland/ClairvoyanceMonad 24 5 months ago The Coq formalization of the paper Reasoning about the garden of forking paths
formal-land/coq-bonsai 24 about 3 years ago 🌳 Generate a fresh bonsai in your terminal
arthuraa/deriving 24 7 months ago Class instances for Coq inductive types with little boilerplate
uwplse/cheerios 23 about 1 year ago Formally verified Coq serialization library with support for extraction to OCaml
sweirich/graded-haskell 23 over 1 year ago Graded Dependent Type systems
math-comp/mczify 23 2 months ago Micromega tactics for Mathematical Components
dunnl/tealeaves 23 about 2 months ago A Coq library for abstract syntactical reasoning
coq-io/system 23 about 5 years ago Library of Unix effects for Coq
coq-community/atbr 23 about 1 month ago Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
thery/T2048 22 about 1 year ago a version of the 2048 game for Coq
sifive/ProcKami 22 over 4 years ago Kami based processor implementations and specifications
rocq-archive/zfc 22 almost 2 years ago An encoding of Zermelo-Fraenkel Set Theory in Coq
pi8027/stablesort 22 2 months ago Stable sort algorithms and their stability proofs in Coq
huynhtrankhanh/CoqCP 22 4 days ago We combat sloppy arguments in competitive programming and raise the standard of rigor
Coq-Polyhedra/Coq-Polyhedra 22 5 months ago Formalizing convex polyhedra in Coq
coq-community/bits 22 4 months ago A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
coq-community/bignums 22 4 months ago Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
bobatkey/system-f-parametricity-model 22 over 9 years ago A Model of Relationally Parametric System F in Coq
Yosuke-Ito-345/Actuary 21 about 1 year ago Formalization of the basic actuarial mathematics using Coq
xavierleroy/cdf-sem-meca 21 7 months ago Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020
weakmemory/imm 21 3 months ago Intermediate Memory Model (IMM) and compilation correctness proofs for it
uwplse/StructTact 21 12 months ago Coq utility and tactic library
kai-qu/linear-logic 21 almost 3 years ago An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
Huxpro/WasmCert 21 about 3 years ago A (in-development) Coq mechanization of WebAssembly specification
coq-community/coqoban 21 almost 2 years ago Sokoban (in Coq) [maintainer=@erikmd]
mmcco/verified-parser-example 20 over 9 years ago A minimal example of a formally verified parser using ocamllex and Menhir's Coq backend
mgrabovsky/fm-notes 20 9 months ago Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Matafou/LibHyps 20 11 months ago A Coq library providing tactics to deal with hypothesis
jwiegley/coq-lattice 20 about 1 year ago A reflection-based proof tactic for lattices in Coq
coq-community/sudoku 20 about 2 years ago A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
CertiKOS/coqrel 20 27 days ago Binary logical relations library for the Coq proof assistant
ejgallego/coq-serapi 128 8 days ago Coq Protocol Playground with Se(xp)rialization of Internal Structures
coq-contribs/coq-in-coq 66 4 months ago A formalisation of the Calculus of Constructions
coq-contribs/zfc 22 almost 2 years ago An encoding of Zermelo-Fraenkel Set Theory in Coq
tchajed/coq-tricks 503 3 months ago Tricks you wish the Coq manual told you
andrejbauer/dedekind-reals 43 4 months ago A formalization of the Dedekind reals in Coq
vellvm/vellvm 400 6 days ago The Vellvm (Verified LLVM) coq development
gallais/parseque 42 11 months ago Total Parser Combinators in Coq
palmskog/coq-program-verification-template 29 4 months ago Template project for program verification in Coq
Blaisorblade/dot-iris 30 15 days ago Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
LogicalAtomist/principia 207 6 months ago The Principia Rewrite
certichain/toychain 111 over 4 years ago A minimalistic blockchain consensus implemented and verified in Coq
coq-community/coq-100-theorems 55 8 months ago Statements of famous theorems proven in Coq [maintainer=@jmadiot]
smtcoq/smtcoq 156 2 months ago Communication between Coq and SAT/SMT solvers
smorimoto/coq-to-ocaml-to-js 25 over 2 years ago Proof of concept to generate safe and fast JavaScript
certichain/ceramist 121 over 4 years ago Verified hash-based AMQ structures in Coq
math-comp/fourcolor 166 7 days ago Formal proof of the Four Color Theorem
foobar-land/coq-bonsai 24 about 3 years ago 🌳 Generate a fresh bonsai in your terminal
bedrocksystems/cpp2v 69 9 days ago Formalization of C++ for verification purposes
hivert/Coq-Combi 1 over 1 year ago Algebraic Combinatorics in Coq
Karmaki/coq-dpdgraph 86 8 days ago Build dependency graphs between COQ objects
CoqEAL/CoqEAL 66 3 months ago CoqEAL -- The Coq Effective Algebra Library
heades/System-F-Coq 19 almost 10 years ago System F in coq
math-comp/hierarchy-builder 97 10 days ago High level commands to declare a hierarchy based on packed classes
project-oak/oak-hardware 124 over 2 years ago Formal specification and verification of hardware, especially for security and privacy
coq-community/coq100 55 8 months ago Statements of famous theorems proven in Coq [maintainer=@jmadiot]
ANSSI-FR/FreeSpec 52 10 months ago A framework for implementing and certifying impure computations in Coq
uds-psl/autosubst 52 2 months ago Automation for de Bruijn syntax and substitution in Coq
uwplse/ornamental-search 49 2 months ago DEVOID: Ornaments for Proof Reuse in Coq
coq-ext-lib/coq-ext-lib 129 2 months ago A library of Coq definitions, theorems, and tactics
siddharthist/coq-big-o 35 over 7 years ago A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces
hazelgrove/hazel 802 6 days ago Hazel, a live functional programming environment with typed holes
Template-Coq/template-coq 382 5 days ago Reflection library for Coq
math-classes/math-classes 162 18 days ago A library of abstract interfaces for mathematical structures in Coq
c-corn/corn 111 8 days ago Coq Repository at Nijmegen
stepchowfun/coq-fun 291 24 days ago A selection of Coq developments
uwdb/Cosette 666 almost 3 years ago Cosette is an automated SQL solver powered by Coq and Rosette
DDCSF/iron 141 over 4 years ago Coq formalizations of functional languages
vladimirias/Foundations 53 about 10 years ago Development of the univalent foundations of mathematics in Coq
aspiwack/cosa 4 over 10 years ago Coq-verified Shape Analysis
Ptival/HaysTac 5 over 6 years ago A pile of Ltac tactics that might contain the needle you're looking for. Oriented around nameless tactics programming
EugeneLoy/coq_jupyter 94 3 months ago Jupyter Notebook kernel for Coq

Backlinks from these awesome lists:

More related projects: