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