awesome-coq

Formal system toolkit

A curated list of libraries and resources for building and verifying formal mathematical systems

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

GitHub
317 stars
14 watching
20 forks
last commit: 3 months ago
Linked from 2 awesome lists

awesomeawesome-listcoqresources

Screenshot of coq-community/awesome-coq website

coq-community.org/awesome-coq

Awesome Coq / Projects / Frameworks
ConCert 114 6 days ago Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages
CoqEAL 66 3 months ago Framework to ease change of data representations in proofs
FCF 48 7 months ago Framework for proofs of cryptography
Fiat 147 about 1 month ago Mostly automated synthesis of correct-by-construction programs
FreeSpec 52 10 months ago Framework for modularly verifying programs with effects and effect handlers
Hoare Type Theory 69 about 1 month ago A shallow embedding of sequential separation logic formulated as a type theory
Hybrid System for reasoning using higher-order abstract syntax representations of object logics
Iris Higher-order concurrent separation logic framework
Q*cert 56 4 months ago Platform for implementing and verifying query compilers
SSProve 56 20 days ago Framework for modular cryptographic proofs based on the Mathematical Components library
VCFloat 24 4 months ago Framework for verifying C programs with floating-point computations
Verdi 589 6 months ago Framework for formally verifying distributed systems implementations
VST Toolchain for verifying C code inside Coq in a higher-order concurrent, impredicative separation logic that is sound w.r.t. the Clight language of the CompCert compiler

Awesome Coq / Projects / User Interfaces
CoqIDE Standalone graphical tool for interacting with Coq
Coqtail 274 2 months ago Interface for Coq based on the Vim text editor
Coq LSP 152 6 days ago Language server and extension for the Visual Studio Code and VSCodium editors with custom document checking engine
Proof General Generic interface for proof assistants based on the extensible, customizable text editor Emacs
Company-Coq 354 almost 2 years ago IDE extensions for Proof General's Coq mode
opam-switch-mode 5 over 1 year ago IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command
jsCoq 515 28 days ago Port of Coq to JavaScript, which enables running Coq projects in a browser
Jupyter kernel for Coq 94 3 months ago Coq support for the Jupyter Notebook web environment
VsCoq 343 8 days ago Language server and extension for the Visual Studio Code and VSCodium editors
VsCoq Legacy 343 8 days ago Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol
Waterproof editor 39 8 months ago Educational environment for writing mathematical proofs in interactive notebooks

Awesome Coq / Projects / Libraries
ALEA 25 about 3 years ago Library for reasoning on randomized algorithms
Algebra Tactics 32 2 months ago Ring and field tactics for Mathematical Components
Bignums 22 4 months ago Library of arbitrarily large numbers
Bedrock Bit Vectors 27 9 months ago Library for reasoning on fixed precision machine words
CertiGraph 17 17 days ago Library for reasoning about directed graphs and their embedding in separation logic
CoLoR 35 18 days ago Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library
coq-haskell 167 about 1 year ago Library smoothing the transition to Coq for Haskell users
Coq-Kruskal 0 6 months ago Collection of libraries related to rose trees and Kruskal's tree theorem
CoqInterval Tactics for performing proofs of inequalities on expressions of real numbers
Coq record update 42 3 months ago Library which provides a generic way to update Coq record fields
Coq-std++ Extended alternative standard library for Coq
ExtLib 129 2 months ago Collection of theories and plugins that may be useful in other Coq developments
FCSL-PCM 26 20 days ago Formalization of partial commutative monoids as used in verification of pointer-manipulating programs
Flocq Formalization of floating-point numbers and computations
Formalised Undecidable Problems 111 about 2 months ago Library of undecidable problems and reductions between them
Hahn 30 5 months ago Library for reasoning on lists and binary relations
Interaction Trees 203 about 1 month ago Library for representing recursive and impure programs
LibHyps 20 11 months ago Library of Ltac tactics to manage and manipulate hypotheses in proofs
MathComp Extra 5 about 1 month ago Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption
Mczify 23 2 months ago Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions
Metalib 71 5 months ago Library for programming language metatheory using locally nameless variable binding representations
Paco Library for parameterized coinduction
Regular Language Representations 41 4 months ago Translations between different definitions of regular languages, including regular expressions and automata
Relation Algebra 48 8 days ago Modular formalization of algebras with heterogeneous binary relations as models
Simple IO 31 2 months ago Input/output monad with user-definable primitive operations
TLC 38 22 days ago Non-constructive alternative to Coq's standard library

Awesome Coq / Projects / Package and Build Management
coq_makefile Build tool distributed with Coq and based on generating a makefile
Coq Nix Toolbox 33 6 days ago Nix helper scripts to automate local builds and continuous integration for Coq
Coq Package Index Collection of Coq packages based on opam
Coq Platform 188 6 days ago Curated collection of packages to support Coq use in industry, education, and research
coq-community Templates 13 about 1 month ago Templates for generating configuration files for Coq projects
Debian Coq packages Coq-related packages available in the testing distribution of Debian
Docker-Coq 37 2 months ago Docker images for many versions of Coq
Docker-MathComp 6 about 1 month ago Docker images for many combinations of versions of Coq and the Mathematical Components library
Docker-Coq GitHub Action GitHub container action that can be used with Docker-Coq or Docker-MathComp
Dune Composable and opinionated build system for OCaml and Coq (former jbuilder)
Nix Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks
Nix Coq packages Collection of Coq-related packages for Nix
opam Flexible and Git-friendly package manager for OCaml and Coq with multiple compiler support

Awesome Coq / Projects / Plugins
AAC Tactics 29 20 days ago Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator
Coinduction 15 2 months ago Plugin for doing proofs by enhanced coinduction
Coq-Elpi 139 6 days ago Extension framework based on λProlog providing an extensive API to implement commands and tactics
CoqHammer 218 6 days ago General-purpose automated reasoning hammer tool that combines learning from previous proofs with the translation of problems to automated provers and the reconstruction of found proofs
Equations 223 9 days ago Function definition package for Coq
Gappa Tactic for discharging goals about floating-point arithmetic and round-off errors
Hierarchy Builder 97 9 days ago Collection of commands for declaring Coq hierarchies based on packed classes
Itauto SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic
Ltac2 Experimental typed tactic language similar to Coq's classic Ltac language
MetaCoq 382 5 days ago Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins
Mtac2 51 about 1 month ago Plugin adding typed tactics for backward reasoning
Paramcoq 44 2 months ago Plugin to generate parametricity translations of Coq terms
QuickChick 254 20 days ago Plugin for randomized property-based testing
SMTCoq 156 2 months ago Tool that checks proof witnesses coming from external SAT and SMT solvers
Tactician Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully
Unicoq 49 5 months ago Plugin that replaces the existing unification algorithm with an enhanced one
Waterproof proof language 33 8 days ago Plugin providing a language for writing proof scripts in a style that resembles non-mechanized mathematical proof

Awesome Coq / Projects / Puzzles and Games
Coqoban 21 almost 2 years ago Coq implementation of Sokoban, the Japanese warehouse keepers' game
Hanoi 24 about 1 year ago The Tower of Hanoi puzzle in Coq, including generalizations and theorems about configurations
Mini-Rubik 4 over 1 year ago Coq formalization and solver of the 2x2x2 version of the Rubik's Cube puzzle
Name the Biggest Number 63 about 2 years ago Repository for submitting proven contenders for the title of biggest number in Coq
Natural Number Game 6 about 2 years ago Coq version of the natural number game developed for the Lean prover
Sudoku 20 about 2 years ago Formalization and solver of the Sudoku number-placement puzzle in Coq
T2048 22 about 1 year ago Coq version of the 2048 sliding tile game

Awesome Coq / Projects / Tools
Alectryon 236 2 months ago Collection of tools for writing technical documents that mix Coq code and prose
Autosubst 2 17 over 1 year ago Tool that generates Coq code for handling binders in syntax, such as for renaming and substitutions
CFML Tool for proving properties of OCaml programs in separation logic
coq2html 30 3 months ago Alternative HTML documentation generator for Coq
coqdoc Standard documentation tool that generates LaTeX or HTML files from Coq code
CoqOfOCaml 255 4 months ago Tool for generating idiomatic Coq from OCaml code
coq-dpdgraph 86 8 days ago Tool for building dependency graphs between Coq objects
coq-scripts 8 about 1 month ago Scripts for dealing with Coq files, including tabulating proof times
coq-tools 39 27 days ago Scripts for manipulating Coq developments

Awesome Coq / Projects / Tools / coq-tools
find-bug.py 39 27 days ago Automatically minimizes source files producing an error, creating small test cases for Coq bugs
absolutize-imports.py 39 27 days ago Processes source files to make loading of dependencies robust against shadowing of file names
inline-imports.py 39 27 days ago Creates stand-alone source files from developments by inlining the loading of all dependencies
minimize-requires.py 39 27 days ago Removes loading of unused dependencies
move-requires.py 39 27 days ago Moves all dependency loading statements to the top of source files
move-vernaculars.py 39 27 days ago Lifts many vernacular commands and inner lemmas out of proof script blocks
proof-using-helper.py 39 27 days ago Modifies source files to include proof annotations for faster parallel proving

Awesome Coq / Projects / Tools
Cosette 666 almost 3 years ago Automated solver for reasoning about SQL query equivalences
hs-to-coq 78 3 months ago Converter from Haskell code to equivalent Coq code
lngen 30 about 1 month ago Tool for generating locally nameless Coq definitions and proofs
Menhir Parser generator that can output Coq code for verified parsers
mCoq 30 about 4 years ago Mutation analysis tool for Coq projects
Ott 347 2 months ago Tool for writing definitions of programming languages and calculi that can be translated to Coq
PyCoq 50 almost 3 years ago Set of bindings and libraries for interacting with Coq from inside Python 3
Roosterize 18 about 2 years ago Tool for suggesting lemma names in Coq projects
Sail 618 6 days ago Tool for specifying instruction set architecture (ISA) semantics of processors and generating Coq definitions
SerAPI 128 8 days ago Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions
Trakt 14 30 days ago Generic goal preprocessing tool for proof automation tactics

Awesome Coq / Projects / Type Theory and Mathematics
Analysis 206 6 days ago Library for classical real analysis compatible with Mathematical Components
Category Theory in Coq 754 about 2 months ago Axiom-free formalization of category theory
Completeness and Decidability of Modal Logic Calculi 8 3 months ago Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL
CoqPrime 37 15 days ago Library for certifying primality using Pocklington and Elliptic Curve certificates
CoRN 111 8 days ago Library of constructive real analysis and algebra
Coqtail Math 15 4 months ago Library of mathematical results ranging from arithmetic to real and complex analysis
Coquelicot Formalization of classical real analysis compatible with the standard library and focusing on usability
Finmap 46 6 months ago Extension of Mathematical Components with finite maps, sets, and multisets
Four Color Theorem 166 6 days ago Formal proof of the Four Color Theorem, a landmark result of graph theory
Gaia 28 3 months ago Implementation of books from Bourbaki's Elements of Mathematics, including set theory and number theory
GeoCoq 186 6 months ago Formalization of geometry based on Tarski's axiom system
Graph Theory 34 4 months ago Formalized graph theory results
Homotopy Type Theory 1,252 14 days ago Development of homotopy-theoretic ideas
Infotheo 64 6 days ago Formalization of information theory and linear error-correcting codes
Mathematical Components Formalization of mathematical theories, focusing in particular on group theory
Math Classes 162 18 days ago Abstract interfaces for mathematical structures based on type classes
Monae 68 27 days ago Monadic effects and equational reasoning
Odd Order Theorem 25 22 days ago Formal proof of the Odd Order Theorem, a landmark result of finite group theory
Puiseuxth 4 about 2 months ago Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series
UniMath 961 9 days ago Library which aims to formalize a substantial body of mathematics using the univalent point of view

Awesome Coq / Projects / Verified Software
CompCert High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors
Ceramist 121 over 4 years ago Verified hash-based approximate membership structures such as Bloom filters
CertiCoq 136 3 months ago Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language
Fiat-Crypto 715 10 days ago Cryptographic primitive code generation
Functional Algorithms Verified in SSReflect 45 7 days ago Purely functional verified implementations of algorithms for searching, sorting, and other fundamental problems
Incremental Cycles Verified OCaml implementation of an algorithm for incremental cycle detection in graphs
Jasmin 269 5 days ago Formalized language and verified compiler for high-assurance and high-speed cryptography
JSCert 196 10 months ago Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
lambda-rust Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries
Prosa Definitions and proofs for real-time system schedulability analysis
RISC-V Specification in Coq 109 4 months ago Definition of the RISC-V processor instruction set architecture and extensions
Stable sort algorithms in Coq 22 2 months ago Generic and modular proofs of correctness, including stability, of mergesort functions
Tarjan and Kosaraju 13 over 1 year ago Verified implementations of algorithms for topological sorting and finding strongly connected components in finite graphs
Vélus Verified compiler for a Lustre/Scade-like dataflow synchronous language
Verdi Raft 183 12 months ago Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
WasmCert-Coq 95 14 days ago Formalization in Coq of the WebAssembly (aka Wasm) 1.0 specification

Awesome Coq / Resources / Community
Official Coq website
Official Coq manual
Official Coq standard library
Official Coq Discourse forum
Official Coq Zulip chat
Official Coq-Club mailing list
Official Coq wiki 4,859 6 days ago
Official Coq X/Twitter
Coq Zulip chat archive
Coq subreddit
Coq tag on Stack Overflow
Coq tag on Theoretical Computer Science Stack Exchange
Coq tag on Proof Assistants Stack Exchange
Coq keyword on Zenodo
Coq-community package maintenance project 68 7 months ago
Mathematical Components wiki 587 6 days ago
100 famous theorems proved using Coq 55 8 months ago
Planet Coq link aggregator

Awesome Coq / Resources / Blogs
Coq Exchange: ideas and experiment reports about Coq
Gagallium
Gregory Malecha's blog
Joachim Breitner's blog posts on Coq
Lysxia's blog
MIT PLV blog posts on Coq
PLClub Blog
Poleiro: a Coq blog by Arthur Azevedo de Amorim
Ralf Jung's blog posts on Coq
Thomas Letan's blog posts on Coq

Awesome Coq / Resources / Books
Coq'Art The first book dedicated to Coq
Software Foundations Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners
Certified Programming with Dependent Types Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof
Program Logics for Certified Compilers Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples
Formal Reasoning About Programs Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose
Programs and Proofs Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language
Computer Arithmetic and Formal Proofs Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library
The Mathematical Components book Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language
Modeling and Proving in Computational Type Theory 80 4 months ago Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming
Hydras & Co. 68 9 months ago Continuously in-progress book and library on Kirby and Paris' hydra battles and other entertaining formalized mathematics in Coq, including a proof of the Gödel-Rosser first incompleteness theorem

Awesome Coq / Resources / Course Material
An Introduction to MathComp-Analysis Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis
Foundations of Separation Logic Introduction to using separation logic to reason about sequential imperative programs in Coq
Floating-Point Numbers and Formal Proof 6 almost 2 years ago Introductory course on Coq real numbers and floating-point numbers from the Flocq library
Introduction to the Theory of Computation Formalization to support an undergraduate course on the theory of computation, including languages and Turing machines
Lectures on Software Foundations 115 7 months ago Material on the Software Foundations series of textbooks, including a series of YouTube videos
MathComp School 6 almost 2 years ago Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library
Mechanized Semantics 64 8 months ago Companion Coq sources for a course on programming language semantics at Collège de France
Program Logics 40 over 3 years ago Companion Coq sources for a course on program logics at Collège de France
Program verification with types and logic Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen
Proofs and Reliable Programming using Coq Introduction to developing and verifying programs with Coq

Awesome Coq / Resources / Tutorials and Hints
Coq'Art Exercises and Tutorials 110 4 months ago Coq code and exercises from the Coq'Art book, including additional tutorials
Coq in a Hurry Introduction to how Coq can be used to define logical concepts and functions and reason about them
Coq requirements in Common Criteria evaluations Guide on how to write readable and reviewable Coq code in high assurance applications
Coq Tactics in Plain English Guide to Coq tactics with explanations and examples
Learn X in Y minutes where X=Coq Whirlwind tour of Coq as a language
Lemma Overloading 26 8 days ago Demonstration of design patterns for programming and proving with canonical structures
MathComp Tutorial Materials 17 about 1 year ago Source code for Mathematical Components tutorials
Mike Nahas's Coq Tutorial Basics of using Coq to write formal proofs
Tricks in Coq 503 3 months ago Tips, tricks, and features in Coq that are hard to discover

Backlinks from these awesome lists:

More related projects: