awesome-coq

Coq toolkit

A curated collection of tools and libraries for formal verification and development in the Coq proof assistant

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

GitHub

235 stars
22 watching
16 forks
last commit: almost 2 years ago
Linked from 1 awesome list


awesome-coq

AbsInt/CompCert1,901almost 2 years agoThe CompCert formally-verified C compiler
HoTT/Coq-HoTT1,262almost 2 years agoA Coq library for Homotopy Type Theory
UniMath/UniMath964almost 2 years agoThis coq library aims to formalize a substantial body of mathematics using the univalent point of view
magmide/magmide810over 2 years agoA dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers
jwiegley/category-theory759almost 2 years agoAn axiom-free formalization of category theory in Coq for personal study and practical work
uwplse/verdi595over 2 years agoA framework for formally verifying distributed systems implementations in Coq
math-comp/math-comp593almost 2 years agoMathematical Components
coq-community/coq-tricks507about 2 years agoTricks you wish the Coq manual told you [maintainer=@tchajed]
PrincetonUniversity/VST444almost 2 years agoVerified Software Toolchain
formal-land/coq-of-rust437over 1 year agoFormal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
MetaCoq/metacoq396almost 2 years agoMetaprogramming, verified meta-theory and implementation of Coq in Coq
princeton-vl/CoqGym388about 3 years agoA Learning Environment for Theorem Proving with the Coq proof assistant
stepchowfun/proofs292over 1 year agoMy personal repository of formally verified mathematics
antalsz/hs-to-coq279almost 6 years agoConvert Haskell source code to Coq source code
jasmin-lang/jasmin275over 1 year agoLanguage for high-assurance and high-speed cryptography
QuickChick/QuickChick259almost 2 years agoRandomized Property-Based Testing Plugin for Coq
UniMath/Foundations241about 12 years agoVoevodsky's original development of the univalent foundations of mathematics in Coq
mit-pdos/fscq237almost 4 years agoFSCQ is a certified file system written and proven in Coq
mattam82/Coq-Equations223almost 2 years agoA function definition package for Coq
math-comp/analysis210almost 2 years agoMathematical Components compliant Analysis Library
DeepSpec/InteractionTrees206almost 2 years agoA Library for Representing Recursive and Impure Programs in Coq
sifive/Kami198about 6 years agoKami - 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/jscert196over 2 years agoA Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
uwplse/verdi-raft186almost 3 years agoAn implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
GeoCoq/GeoCoq186over 2 years agoA formalization of geometry in Coq based on Tarski's axiom system
clarus/coq-chick-blog178almost 7 years ago🐣 A blog engine written and proven in Coq
coq-community/fourcolor174almost 2 years agoFormal proof of the Four Color Theorem [maintainer=@ybertot]
jwiegley/coq-haskell168almost 3 years agoA library for formalizing Haskell types and functions in Coq
mit-pdos/perennial165over 1 year agoVerifying concurrent crash-safe systems
coq-community/math-classes162almost 2 years agoA library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
ilyasergey/pnp160about 5 years agoLecture notes for a short course on proving/programming in Coq via SSReflect
mit-plv/koika143almost 2 years agoA core language for rule-based hardware design 🦑
mit-plv/kami143almost 2 years agoA Platform for High-Level Parametric Hardware Specification and its Modular Verification
barry-jay-personal/tree-calculus143over 5 years agoProofs in Coq for the book Reflective Programs in Tree Calculus
discus-lang/iron142about 6 years agoCoq formalizations of functional languages
Lysxia/advent-of-coq-2018140over 7 years agoAdvent of Code 2018, in Coq! ( )
CertiCoq/certicoq137about 2 years agoA Verified Compiler for Gallina, Written in Gallina
coq-community/coq-ext-lib129almost 2 years agoA library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
rocq-archive/coq-serapi128almost 2 years agoCoq Protocol Playground with Se(xp)rialization of Internal Structures
project-oak/silveroak123over 4 years agoFormal specification and verification of hardware, especially for security and privacy
verse-lab/ceramist121over 6 years agoVerified hash-based AMQ structures in Coq
coq-community/coq-art114about 2 years agoCoq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
AU-COBRA/ConCert114almost 2 years agoA framework for smart contract verification in Coq
verse-lab/toychain111over 6 years agoA minimalistic blockchain consensus implemented and verified in Coq
uds-psl/coq-library-undecidability111almost 2 years agoA library of mechanised undecidability proofs in the Coq proof assistant
coq-community/corn111almost 2 years agoCoq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
mit-plv/riscv-coq110about 2 years agoRISC-V Specification in Coq
Ptival/PeaCoq106about 5 years agoPeaCoq is a pretty Coq, isn't it?
WasmCert/WasmCert-Coq100almost 2 years agoA mechanisation of Wasm in Coq
sec-bit/tokenlibs-with-proofs97over 7 years agoCorrectness proofs of Ethereum token contracts
DistributedComponents/disel95about 2 years agoDistributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
amintimany/Categories94almost 2 years agoA formalization of category theory in the Coq proof assistant
clarus/falso93almost 7 years agoA proof of false in Coq
ymherklotz/vericert88about 2 years agoA formally verified high-level synthesis tool based on CompCert and written in Coq
coq-community/coq-dpdgraph87almost 2 years agoBuild dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
coq-concurrency/pluto86about 10 years agoA web server written in Coq
inQWIRE/SQIR80about 2 years agoA Small Quantum Intermediate Representation
plclub/hs-to-coq79about 2 years agoConvert Haskell source code to Coq source code
pi8027/lambda-calculus78about 6 years agoA Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
ml4tp/gamepad72about 4 years agoA Learning Environment for Theorem Proving
bluerock-io/BRiCk72almost 2 years agoFormalization of C++ for verification purposes
imdea-software/htt70almost 2 years agoHoare Type Theory
affeldt-aist/monae70almost 2 years agoMonadic effects and equational reasonig in Coq
coq-community/hydra-battles69over 2 years agoVariations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
coq-community/coqeal67almost 2 years agoThe Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
rocq-archive/coq-in-coq66about 2 years agoA formalisation of the Calculus of Constructions
xavierleroy/cdf-mech-sem64over 2 years agoCoq development for the course "Mechanized semantics", Collège de France, 2019-2020
coq-io/io64over 4 years agoA library for effects in Coq
affeldt-aist/infotheo64almost 2 years agoA Coq formalization of information theory and linear error-correcting codes
INRIA/velus63almost 2 years agoA Lustre compiler in Coq
choukh/Set-Theory59almost 5 years agoA formalization of the textbook Elements of Set Theory
sigurdschneider/lvc57almost 8 years agoLVC verified compiler
mit-plv/bedrock57over 9 years agoCoq library for verified low-level programming
SSProve/ssprove56almost 2 years agoA foundational framework for modular cryptographic proofs in Coq
philzook58/nand2coq54over 4 years agoBuild an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools)
geohot/coq-hardy53over 7 years agoFormalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
lthms/FreeSpec52over 2 years agoA framework for implementing and certifying impure computations in Coq
coq-community/autosubst52almost 2 years agoAutomation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
mit-plv/rupicola51almost 2 years agoGallina to Bedrock2 compilation toolkit
MichaelBurge/pornview51about 9 years agoPorn browser formally-verified in Coq
jtassarotti/coq-proba50almost 3 years agoA Probability Theory Library for the Coq Theorem Prover
anton-trunov/coq-lecture-notes50almost 6 years agoCoq Lecture Notes (WIP)
uwplse/pumpkin-pi49almost 2 years agoAn extension to PUMPKIN PATCH with support for proof repair across type equivalences
tchajed/iris-simp-lang49over 2 years agoWe define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic
cmeiklejohn/distributed-data-structures49almost 13 years agoDistributed Data Structures in Coq
damien-pous/relation-algebra48almost 2 years agoRelation algebra library for Coq
math-comp/finmap47over 2 years agoFinite sets, finite maps, multisets and generic sets
coq-community/topology47almost 2 years agoGeneral topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
arthuraa/poleiro47over 4 years agoA blog about Coq
foreverbell/verified46over 8 years agoCoq formalizations and proofs of (data) structures and algorithms
coq-community/semantics46almost 5 years agoA survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
coq-community/paramcoq45almost 2 years agoCoq plugin for parametricity [maintainer=@proux01]
coq-community/fav-ssr45almost 2 years agoFunctional Algorithms Verified in SSReflect [maintainer=@clayrat]
vrahli/NuprlInCoq44almost 2 years agoImplementation of Nuprl's type theory in Coq
pirapira/evmverif44almost 10 years agoAn EVM code verification framework in Coq
dschepler/coq-sequent-calculus44over 10 years agoCoq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic
wouter-swierstra/xmonad43about 14 years agoxmonad in Coq
tchajed/ltac2-tutorial43almost 4 years agoLtac2 tutorial
tchajed/coq-record-update43about 2 years agoLibrary to create Coq record update functions
snu-sf/paco43almost 2 years agoA Coq library for parametric coinduction
coq-community/dedekind-reals43about 2 years agoA formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
choukh/Baby-Set-Theory43over 4 years agoCoq集合论中文教程
mit-plv/coqutil42almost 2 years agoCoq library for tactics, basic definitions, sets, maps
coq-community/parseque42over 2 years agoTotal Parser Combinators in Coq [maintainer=@womeier]
coq-community/reglang41about 2 years agoRegular Language Representations in Coq [maintainers=@chdoc,@palmskog]
xavierleroy/cdf-program-logics40over 5 years agoCompanion Coq development for Xavier Leroy's 2021 lectures on program logics
meithecatte/busycoq39about 2 years agoBusy Beaver deciders backed by Coq proof
CertiCoq/VeriFFI39about 2 years agoVeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project
vlopezj/coq-course38about 9 years agoCoq course at Chalmers CSE
charguer/tlc38almost 2 years agoLibrary for Classical Coq
thery/coqprime37almost 2 years agoPrime numbers for Coq
math-comp/Coq-Combi37almost 2 years agoAlgebraic Combinatorics in Coq
takanuva/cps36almost 2 years agoA formalization of continuation-passing style calculi in Coq [WIP]
gangtan/CPUmodels36about 9 years agoGoNative project: formal machines models in Coq
langston-barrett/coq-big-o35over 9 years agoA general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces
fblanqui/color35almost 2 years agoCoq library on rewriting theory and termination
coq-community/graph-theory35almost 2 years agoGraph Theory [maintainers=@chdoc,@damien-pous]
snu-sf/promising-coq33almost 2 years agoThe Coq development of A Promising Semantics for Relaxed-Memory Concurrency
pedrotst/coquedille33almost 6 years agoA Coq to Cedille compiler written in Coq
math-comp/algebra-tactics33almost 2 years agoRing, field, lra, nra, and psatz tactics for Mathematical Components
marshall-lee/software_foundations33about 2 years agoMy solutions to Software Foundations course in Coq proof assistant
Lysxia/system-F33over 7 years agoFormalization of the polymorphic lambda calculus and its parametricity theorem
logsem/aneris33over 1 year agoProgram logic for developing and verifying distributed systems
impermeable/coq-waterproof33almost 2 years agoThe 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/certicrypt33over 10 years agoCertiCrypt Coq Framework
inQWIRE/QuantumLib33almost 2 years agoCoq library for reasoning about quantum programs
coq-community/chapar32over 2 years agoA framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
bmsherman/topology32almost 8 years agoFormal topology (and some probability) in Coq
Lysxia/coq-simple-io31almost 2 years agoIO for Gallina
codyroux/broad-coq-tutorial31almost 5 years agoSome unstructured notes concerning the Broad tutorial to take place in March 2020
vafeiadis/hahn30about 2 years agoHahn: A Coq library
pa-ba/calc-comp30almost 3 years agoCoq proofs for the paper "Calculating Correct Compilers"
formal-land/coq-of-python30about 2 years agoTranslate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python
coq-community/gaia30about 2 years agoImplementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
coq-community/dblib30about 5 years agoCoq library for working with de Bruijn indices [maintainer=@KevOrr]
coq-community/coq-program-verification-template29about 2 years agoTemplate project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
arthuraa/extructures29almost 2 years agoFinite sets and maps for Coq with extensional equality
vrahli/Velisarios28about 7 years agoA Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
tezos/tezoscoq28about 9 years agoworking with coq and tezos
math-comp/Abel28almost 2 years agoA proof of Abel-Ruffini theorem
llee454/functional-algebra28over 7 years agoThis 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/goedel28almost 4 years agoArchived since the contents have been moved to the Hydras & Co. repository
acorrenson/SATurne28over 4 years agoTiny verified SAT-solver
math-comp/odd-order27almost 2 years agoThe formal proof of the Odd Order Theorem
reynir/Brainfuck26over 4 years agoBrainfuck formalized in Coq
novifinancial/LibraChain26over 6 years agoA library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover
imdea-software/fcsl-pcm26almost 2 years agoPartial Commutative Monoids
dboulytchev/miniKanren-coq26almost 6 years agoA certified semantics for relational programming workout
coq-ext-lib/coq-compile26over 13 years agoA compiler for Coq
coq-community/lemma-overloading26almost 2 years agoLibraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
affeldt-aist/coq-robot26over 2 years agoMathematics of Rigid Body Transformationss using Coq and MathComp
rafaelcgs10/W-in-Coq25about 6 years agoThis is a Coq formalization of Damas-Milner type system and its algorithm W
coq-community/alea25almost 5 years agoCoq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
AU-COBRA/PoS-NSB25over 5 years agoA formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq
Zilliqa/scilla-coq24about 6 years agoState-Transition Systems for Smart Contracts
VeriNum/vcfloat24about 2 years agoVCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
thery/hanoi24almost 3 years agoHanoi tower in Coq
sweirich/graded-haskell24about 3 years agoGraded Dependent Type systems
math-comp/mczify24almost 2 years agoMicromega tactics for Mathematical Components
lastland/ClairvoyanceMonad24over 2 years agoThe Coq formalization of the paper Reasoning about the garden of forking paths
formal-land/coq-bonsai24almost 5 years ago🌳 Generate a fresh bonsai in your terminal
arthuraa/deriving24almost 2 years agoClass instances for Coq inductive types with little boilerplate
uwplse/cheerios23almost 3 years agoFormally verified Coq serialization library with support for extraction to OCaml
dunnl/tealeaves23almost 2 years agoA Coq library for abstract syntactical reasoning
coq-io/system23almost 7 years agoLibrary of Unix effects for Coq
coq-community/atbr23almost 2 years agoCoq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
thery/T204822almost 3 years agoa version of the 2048 game for Coq
sifive/ProcKami22over 6 years agoKami based processor implementations and specifications
rocq-archive/zfc22over 3 years agoAn encoding of Zermelo-Fraenkel Set Theory in Coq
pi8027/stablesort22about 2 years agoStable sort algorithms and their stability proofs in Coq
huynhtrankhanh/CoqCP22almost 2 years agoWe combat sloppy arguments in competitive programming and raise the standard of rigor
Coq-Polyhedra/Coq-Polyhedra22about 2 years agoFormalizing convex polyhedra in Coq
coq-community/bits22about 2 years agoA formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
coq-community/bignums22almost 2 years agoCoq 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-model22over 11 years agoA Model of Relationally Parametric System F in Coq
Yosuke-Ito-345/Actuary21almost 2 years agoFormalization of the basic actuarial mathematics using Coq
xavierleroy/cdf-sem-meca21over 2 years agoDéveloppement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020
weakmemory/imm21about 2 years agoIntermediate Memory Model (IMM) and compilation correctness proofs for it
uwplse/StructTact21almost 3 years agoCoq utility and tactic library
mgrabovsky/fm-notes21over 2 years agoUnassorted scribbles on formal methods, type theory, category theory, and so on, and so on
kai-qu/linear-logic21over 4 years agoAn encoding of linear logic in Coq with minimal Sokoban and blocks world examples
Huxpro/WasmCert21almost 5 years agoA (in-development) Coq mechanization of WebAssembly specification
coq-community/coqoban21over 3 years agoSokoban (in Coq) [maintainer=@erikmd]
mmcco/verified-parser-example20over 11 years agoA minimal example of a formally verified parser using ocamllex and Menhir's Coq backend
Matafou/LibHyps20almost 2 years agoA Coq library providing tactics to deal with hypothesis
jwiegley/coq-lattice20almost 3 years agoA reflection-based proof tactic for lattices in Coq
CoqHott/logrel-coq20almost 2 years agoLogical Relation for MLTT in Coq
coq-community/sudoku20almost 4 years agoA certified Sudoku solver in Coq [maintainers=@siraben,@thery]
CertiKOS/coqrel20almost 2 years agoBinary logical relations library for the Coq proof assistant
LPCIC/coq-elpi141almost 2 years agoCoq plugin embedding elpi
bedrocksystems/BRiCk72almost 2 years agoFormalization of C++ for verification purposes
ejgallego/coq-serapi128almost 2 years agoCoq Protocol Playground with Se(xp)rialization of Internal Structures
coq-contribs/coq-in-coq66about 2 years agoA formalisation of the Calculus of Constructions
coq-contribs/zfc22over 3 years agoAn encoding of Zermelo-Fraenkel Set Theory in Coq
tchajed/coq-tricks507about 2 years agoTricks you wish the Coq manual told you
andrejbauer/dedekind-reals43about 2 years agoA formalization of the Dedekind reals in Coq
vellvm/vellvm405almost 2 years agoThe Vellvm (Verified LLVM) coq development
gallais/parseque42over 2 years agoTotal Parser Combinators in Coq
palmskog/coq-program-verification-template29about 2 years agoTemplate project for program verification in Coq
Blaisorblade/dot-iris30almost 2 years agoScala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
LogicalAtomist/principia208over 1 year agoThe Principia Rewrite
certichain/toychain111over 6 years agoA minimalistic blockchain consensus implemented and verified in Coq
coq-community/coq-100-theorems57over 2 years agoStatements of famous theorems proven in Coq [maintainer=@jmadiot]
smtcoq/smtcoq157almost 2 years agoCommunication between Coq and SAT/SMT solvers
smorimoto/coq-to-ocaml-to-js24about 4 years agoProof of concept to generate safe and fast JavaScript
certichain/ceramist121over 6 years agoVerified hash-based AMQ structures in Coq
math-comp/fourcolor174almost 2 years agoFormal proof of the Four Color Theorem
foobar-land/coq-bonsai24almost 5 years ago🌳 Generate a fresh bonsai in your terminal
bedrocksystems/cpp2v72almost 2 years agoFormalization of C++ for verification purposes
hivert/Coq-Combi1over 3 years agoAlgebraic Combinatorics in Coq
Karmaki/coq-dpdgraph87almost 2 years agoBuild dependency graphs between COQ objects
CoqEAL/CoqEAL67almost 2 years agoCoqEAL -- The Coq Effective Algebra Library
heades/System-F-Coq19over 11 years agoSystem F in coq
math-comp/hierarchy-builder97almost 2 years agoHigh level commands to declare a hierarchy based on packed classes
project-oak/oak-hardware123over 4 years agoFormal specification and verification of hardware, especially for security and privacy
coq-community/coq10057over 2 years agoStatements of famous theorems proven in Coq [maintainer=@jmadiot]
ANSSI-FR/FreeSpec52over 2 years agoA framework for implementing and certifying impure computations in Coq
uds-psl/autosubst52almost 2 years agoAutomation for de Bruijn syntax and substitution in Coq
uwplse/ornamental-search49almost 2 years agoDEVOID: Ornaments for Proof Reuse in Coq
coq-ext-lib/coq-ext-lib129almost 2 years agoA library of Coq definitions, theorems, and tactics
siddharthist/coq-big-o35over 9 years agoA general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces
hazelgrove/hazel808almost 2 years agoHazel, a live functional programming environment with typed holes
Template-Coq/template-coq396almost 2 years agoReflection library for Coq
math-classes/math-classes162almost 2 years agoA library of abstract interfaces for mathematical structures in Coq
c-corn/corn111almost 2 years agoCoq Repository at Nijmegen
stepchowfun/coq-fun292over 1 year agoA selection of Coq developments
uwdb/Cosette668over 4 years agoCosette is an automated SQL solver powered by Coq and Rosette
DDCSF/iron142about 6 years agoCoq formalizations of functional languages
vladimirias/Foundations53about 12 years agoDevelopment of the univalent foundations of mathematics in Coq
aspiwack/cosa4about 12 years agoCoq-verified Shape Analysis
Ptival/HaysTac5about 8 years agoA pile of Ltac tactics that might contain the needle you're looking for. Oriented around nameless tactics programming
EugeneLoy/coq_jupyter94about 2 years agoJupyter Notebook kernel for Coq

Backlinks from these awesome lists:

More related projects: