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

Available items

The developer of this repository has not created any items for sale yet. Need a bug fixed? Help with integration? A different license? **Create a request here**:

Readme

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
- antalsz/hs-to-coq - Convert Haskell source code to Coq source code
- tchajed/coq-tricks - Tricks you wish the Coq manual told you
- vellvm/vellvm - The Vellvm (Verified LLVM) coq development.
- 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
- jscert/jscert - A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
- MetaCoq/metacoq - Metaprogramming in Coq
- QuickChick/QuickChick - Randomized Property-Based Testing Plugin for Coq
- clarus/coq-chick-blog - 🐣 A blog engine written and proven in Coq
- princeton-vl/CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant
- 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
- mattam82/Coq-Equations - A function definition package for Coq
- uwplse/verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
- Lysxia/advent-of-coq-2018 - Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
- stepchowfun/proofs - A selection of formal proofs 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 [[email protected]]
- GeoCoq/GeoCoq - A formalization of geometry in Coq based on Tarski's axiom system
- DeepSpec/InteractionTrees - A Library for Representing Recursive and Impure Programs in Coq
- discus-lang/iron - Coq formalizations of functional languages.
- certichain/ceramist - Verified hash-based AMQ structures in Coq
- ilyasergey/pnp - Lecture notes for a short course on proving/programming in Coq via SSReflect.
- Ptival/PeaCoq - PeaCoq is a pretty Coq, isn't it?
- coq-community/corn - Coq Repository at Nijmegen [[email protected],@VincentSe]
- coq-community/coq-ext-lib - A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
- certichain/toychain - A minimalistic blockchain consensus implemented and verified in Coq
- amintimany/Categories - A formalization of category theory in the Coq proof assistant.
- smtcoq/smtcoq - Communication between Coq and SAT/SMT solvers
- DistributedComponents/disel - Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
- math-comp/fourcolor - Formal proof of the Four Color Theorem
- sec-bit/tokenlibs-with-proofs - Correctness proofs of Ethereum token contracts
- coq-concurrency/pluto - A web server written in Coq.
- math-comp/analysis - Mathematical Components compliant Analysis Library
- clarus/falso - A proof of false in Coq.
- ml4tp/gamepad - A Learning Environment for Theorem Proving
- mit-plv/riscv-coq - RISC-V Specification in Coq
- pi8027/lambda-calculus - A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
- Karmaki/coq-dpdgraph - Build dependency graphs between COQ objects
- sigurdschneider/lvc - LVC verified compiler
- coq-io/io - A library for effects in Coq.
- mit-pdos/perennial - Verifying concurrent crash-safe systems
- cmeiklejohn/distributed-data-structures - Distributed Data Structures in Coq
- affeldt-aist/monae - Monadic effects and equational reasonig in Coq
- pirapira/evmverif - An EVM code verification framework in Coq
- anton-trunov/coq-lecture-notes - Coq Lecture Notes (WIP)
- MichaelBurge/pornview - Porn browser formally-verified in Coq
- CoqEAL/CoqEAL - CoqEAL -- The Coq Effective Algebra Library
- ANSSI-FR/FreeSpec - A framework for implementing and certifying impure computations in Coq
- wouter-swierstra/xmonad - xmonad in Coq
- arthuraa/poleiro - A blog about Coq
- uds-psl/coq-library-undecidability - A library of formalised undecidable problems in Coq
- geohot/coq-hardy - Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
- mit-plv/koika - A core language for rule-based hardware design 🦑
- foreverbell/verified - Coq formalizations and proofs of (data) structures and algorithms.
- gallais/parseque - Total Parser Combinators in Coq
- dschepler/coq-sequent-calculus - Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic
- uwplse/pumpkin-pi - An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
- affeldt-aist/infotheo - A Coq formalization of information theory and linear error-correcting codes
- math-comp/finmap - Finite sets, finite maps, multisets and generic sets
- 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/topology - General topology in Coq [[email protected]]
- project-oak/oak-hardware - Formal specification and verification of hardware, especially for security and privacy.
- coq-community/paramcoq - Coq plugin for parametricity [[email protected]]
- INRIA/velus - A Lustre compiler in Coq
- ymherklotz/vericert - A formally verified high-level synthesis tool based on CompCert and written in Coq.
- coq-contribs/coq-in-coq - A formalisation of the Calculus of Constructions
- andrejbauer/dedekind-reals - A formalization of the Dedekind reals in Coq
- mit-plv/bedrock - Coq library for verified low-level programming
- bmsherman/topology - Formal topology (and some probability) in Coq
- vlopezj/coq-course - Coq course at Chalmers CSE
- snu-sf/paco - A Coq library for parametric coinduction
- philzook58/nand2coq - Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
- coq-community/coq-art - Coq code and exercises from the Coq'Art book [[email protected],@Casteran]
- pedrotst/coquedille - A Coq to Cedille compiler written in Coq
- jtassarotti/coq-proba - A Probability Theory Library for the Coq Theorem Prover
- damien-pous/relation-algebra - Relation algebra library for Coq
- coq-community/chapar - A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [[email protected]]
- vrahli/NuprlInCoq - Implementation of Nuprl's type theory in Coq
- tezos/tezoscoq - working with coq and tezos
- coq-ext-lib/coq-compile - A compiler for Coq
- uds-psl/autosubst - Automation for de Bruijn syntax and substitution in Coq
- pa-ba/calc-comp - Coq proofs for the paper "Calculating Correct Compilers"
- tchajed/coq-record-update - Library to create Coq record update functions
- snu-sf/promising-coq - The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
- imdea-software/htt - Hoare Type Theory
- hivert/Coq-Combi - Algebraic Combinatorics in Coq
- haklabbeograd/software-foundations-coq-workshop - Materijal za radionicu Coq-a prema kursu "Software foundations" (CIS 500) Benjamina Piercea
- bedrocksystems/cpp2v - Formalization of C++ for verification purposes.
- tchajed/ltac2-tutorial - Ltac2 tutorial
- gangtan/CPUmodels - GoNative project: formal machines models in Coq
- coq-community/coq100 - Statements of famous theorems proven in Coq [[email protected]]
- vafeiadis/hahn - Hahn: A Coq library
- sifive/ProcKami - Kami based processor implementations and specifications
- 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.
- uwplse/StructTact - Another library oriented around avoiding breakage due to naming changes.
- EugeneLoy/coq_jupyter - Jupyter Notebook kernel for Coq