awesome-coq
by uhub
A curated list of awesome Coq frameworks, libraries and software.
AI summary
Coq toolkit
A curated collection of tools and libraries for formal verification and development in the Coq proof assistant
- stars
- 235
- forks
- 16
- watching
- 22
- awesome list
- 1
- entries
- 232
What's in the list
232 links in 1 sections, with live GitHub stats.activeno commit in 2y
Links
AbsInt/CompCert
The CompCert formally-verified C compiler
HoTT/Coq-HoTT
A Coq library for Homotopy Type Theory
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
coq-community/coq-tricks
Tricks you wish the Coq manual told you [maintainer=@tchajed]
PrincetonUniversity/VST
Verified Software Toolchain
formal-land/coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
MetaCoq/metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
princeton-vl/CoqGym
A Learning Environment for Theorem Proving with the Coq proof assistant
stepchowfun/proofs
My personal repository of formally verified mathematics
antalsz/hs-to-coq
Convert Haskell source code to Coq source code
jasmin-lang/jasmin
Language for high-assurance and high-speed cryptography
QuickChick/QuickChick
Randomized Property-Based Testing Plugin for Coq
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
Mathematical Components compliant Analysis Library
DeepSpec/InteractionTrees
A Library for Representing Recursive and Impure Programs in 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
jscert/jscert
A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
GeoCoq/GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
clarus/coq-chick-blog
🐣 A blog engine written and proven in Coq
Formal proof of the Four Color Theorem [maintainer=@ybertot]
A library for formalizing Haskell types and functions in Coq
Verifying concurrent crash-safe systems
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
ilyasergey/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect
mit-plv/koika
A core language for rule-based hardware design 🦑
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
barry-jay-personal/tree-calculus
Proofs in Coq for the book Reflective Programs in Tree Calculus
discus-lang/iron
Coq formalizations of functional languages
Lysxia/advent-of-coq-2018
Advent of Code 2018, in Coq! ( )
CertiCoq/certicoq
A Verified Compiler for Gallina, Written in Gallina
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
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
AU-COBRA/ConCert
A framework for smart contract verification in Coq
A minimalistic blockchain consensus implemented and verified in Coq
uds-psl/coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
RISC-V Specification in Coq
Ptival/PeaCoq
PeaCoq is a pretty Coq, isn't it?
WasmCert/WasmCert-Coq
A mechanisation of Wasm in Coq
sec-bit/tokenlibs-with-proofs
Correctness proofs of Ethereum token contracts
DistributedComponents/disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
amintimany/Categories
A formalization of category theory in the Coq proof assistant
A proof of false in Coq
ymherklotz/vericert
A formally verified high-level synthesis tool based on CompCert and written in Coq
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
ml4tp/gamepad
A Learning Environment for Theorem Proving
bluerock-io/BRiCk
Formalization of C++ for verification purposes
imdea-software/htt
Hoare Type Theory
affeldt-aist/monae
Monadic effects and equational reasonig in Coq
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
A formalisation of the Calculus of Constructions
xavierleroy/cdf-mech-sem
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
coq-io/io
A library for effects in Coq
A Coq formalization of information theory and linear error-correcting codes
INRIA/velus
A Lustre compiler in Coq
choukh/Set-Theory
A formalization of the textbook Elements of Set Theory
sigurdschneider/lvc
LVC verified compiler
Coq library for verified low-level programming
SSProve/ssprove
A foundational framework for modular cryptographic proofs in Coq
philzook58/nand2coq
Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools)
geohot/coq-hardy
Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
lthms/FreeSpec
A framework for implementing and certifying impure computations in Coq
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Gallina to Bedrock2 compilation toolkit
MichaelBurge/pornview
Porn browser formally-verified in Coq
jtassarotti/coq-proba
A Probability Theory Library for the Coq Theorem Prover
anton-trunov/coq-lecture-notes
Coq Lecture Notes (WIP)
An extension to PUMPKIN PATCH with support for proof repair across type equivalences
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
cmeiklejohn/distributed-data-structures
Distributed Data Structures in Coq
damien-pous/relation-algebra
Relation algebra library for Coq
Finite sets, finite maps, multisets and generic sets
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
arthuraa/poleiro
A blog about Coq
foreverbell/verified
Coq formalizations and proofs of (data) structures and algorithms
A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
Coq plugin for parametricity [maintainer=@proux01]
Functional Algorithms Verified in SSReflect [maintainer=@clayrat]
vrahli/NuprlInCoq
Implementation of Nuprl's type theory in Coq
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
wouter-swierstra/xmonad
xmonad in Coq
Ltac2 tutorial
Library to create Coq record update functions
snu-sf/paco
A Coq library for parametric coinduction
A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
Coq集合论中文教程
Coq library for tactics, basic definitions, sets, maps
Total Parser Combinators in Coq [maintainer=@womeier]
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
Companion Coq development for Xavier Leroy's 2021 lectures on program logics
meithecatte/busycoq
Busy Beaver deciders backed by Coq proof
VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project
vlopezj/coq-course
Coq course at Chalmers CSE
charguer/tlc
Library for Classical Coq
thery/coqprime
Prime numbers for Coq
Algebraic Combinatorics in Coq
takanuva/cps
A formalization of continuation-passing style calculi in Coq [WIP]
gangtan/CPUmodels
GoNative project: formal machines models in Coq
langston-barrett/coq-big-o
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces
fblanqui/color
Coq library on rewriting theory and termination
Graph Theory [maintainers=@chdoc,@damien-pous]
The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
pedrotst/coquedille
A Coq to Cedille compiler written in Coq
Ring, field, lra, nra, and psatz tactics for Mathematical Components
marshall-lee/software_foundations
My solutions to Software Foundations course in Coq proof assistant
Formalization of the polymorphic lambda calculus and its parametricity theorem
logsem/aneris
Program logic for developing and verifying distributed systems
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
EasyCrypt/certicrypt
CertiCrypt Coq Framework
Coq library for reasoning about quantum programs
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
bmsherman/topology
Formal topology (and some probability) in Coq
IO for Gallina
codyroux/broad-coq-tutorial
Some unstructured notes concerning the Broad tutorial to take place in March 2020
vafeiadis/hahn
Hahn: A Coq library
pa-ba/calc-comp
Coq proofs for the paper "Calculating Correct Compilers"
Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Coq library for working with de Bruijn indices [maintainer=@KevOrr]
Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
Finite sets and maps for Coq with extensional equality
A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
tezos/tezoscoq
working with coq and tezos
A proof of Abel-Ruffini theorem
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
Archived since the contents have been moved to the Hydras & Co. repository
acorrenson/SATurne
Tiny verified SAT-solver
The formal proof of the Odd Order Theorem
reynir/Brainfuck
Brainfuck formalized in Coq
novifinancial/LibraChain
A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover
Partial Commutative Monoids
dboulytchev/miniKanren-coq
A certified semantics for relational programming workout
coq-ext-lib/coq-compile
A compiler for Coq
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
Mathematics of Rigid Body Transformationss using Coq and MathComp
rafaelcgs10/W-in-Coq
This is a Coq formalization of Damas-Milner type system and its algorithm W
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq
Zilliqa/scilla-coq
State-Transition Systems for Smart Contracts
VeriNum/vcfloat
VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Hanoi tower in Coq
sweirich/graded-haskell
Graded Dependent Type systems
Micromega tactics for Mathematical Components
lastland/ClairvoyanceMonad
The Coq formalization of the paper Reasoning about the garden of forking paths
🌳 Generate a fresh bonsai in your terminal
Class instances for Coq inductive types with little boilerplate
Formally verified Coq serialization library with support for extraction to OCaml
dunnl/tealeaves
A Coq library for abstract syntactical reasoning
Library of Unix effects for Coq
Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
a version of the 2048 game for Coq
Kami based processor implementations and specifications
An encoding of Zermelo-Fraenkel Set Theory in Coq
Stable sort algorithms and their stability proofs in Coq
huynhtrankhanh/CoqCP
We combat sloppy arguments in competitive programming and raise the standard of rigor
Coq-Polyhedra/Coq-Polyhedra
Formalizing convex polyhedra in Coq
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
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
A Model of Relationally Parametric System F in Coq
Yosuke-Ito-345/Actuary
Formalization of the basic actuarial mathematics using Coq
Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020
weakmemory/imm
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Coq utility and tactic library
mgrabovsky/fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
kai-qu/linear-logic
An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
Huxpro/WasmCert
A (in-development) Coq mechanization of WebAssembly specification
Sokoban (in Coq) [maintainer=@erikmd]
mmcco/verified-parser-example
A minimal example of a formally verified parser using ocamllex and Menhir's Coq backend
Matafou/LibHyps
A Coq library providing tactics to deal with hypothesis
A reflection-based proof tactic for lattices in Coq
CoqHott/logrel-coq
Logical Relation for MLTT in Coq
A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
CertiKOS/coqrel
Binary logical relations library for the Coq proof assistant
LPCIC/coq-elpi
Coq plugin embedding elpi
Formalization of C++ for verification purposes
Coq Protocol Playground with Se(xp)rialization of Internal Structures
A formalisation of the Calculus of Constructions
An encoding of Zermelo-Fraenkel Set Theory in Coq
Tricks you wish the Coq manual told you
A formalization of the Dedekind reals in Coq
vellvm/vellvm
The Vellvm (Verified LLVM) coq development
Total Parser Combinators in Coq
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
A minimalistic blockchain consensus implemented and verified in Coq
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
Verified hash-based AMQ structures in Coq
Formal proof of the Four Color Theorem
🌳 Generate a fresh bonsai in your terminal
Formalization of C++ for verification purposes
hivert/Coq-Combi
Algebraic Combinatorics in Coq
Build dependency graphs between COQ objects
CoqEAL -- The Coq Effective Algebra Library
heades/System-F-Coq
System F in coq
High level commands to declare a hierarchy based on packed classes
Formal specification and verification of hardware, especially for security and privacy
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
A framework for implementing and certifying impure computations in Coq
Automation for de Bruijn syntax and substitution in Coq
DEVOID: Ornaments for Proof Reuse in Coq
A library of Coq definitions, theorems, and tactics
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
Reflection library for Coq
A library of abstract interfaces for mathematical structures in Coq
Coq Repository at Nijmegen
A selection of Coq developments
uwdb/Cosette
Cosette is an automated SQL solver powered by Coq and Rosette
Coq formalizations of functional languages
vladimirias/Foundations
Development of the univalent foundations of mathematics in Coq
aspiwack/cosa
Coq-verified Shape Analysis
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
Nothing in this list matches your filter.
Featured in 1 awesome list
Each link jumps to the spot where the list mentions awesome-coq.
More related projects
williamdemeo/typefunc309
engineeringsoftware/roosterize18
runtimeverification/verified-smart-contracts720
lukaszcz/coqhammer220
ethereum/tests567