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
325 stars
14 watching
20 forks
last commit: about 1 year 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 12 months ago Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages
CoqEAL 67 11 months ago Framework to ease change of data representations in proofs
FCF 48 over 1 year ago Framework for proofs of cryptography
Fiat 149 12 months ago Mostly automated synthesis of correct-by-construction programs
FreeSpec 52 almost 2 years ago Framework for modularly verifying programs with effects and effect handlers
Hoare Type Theory 70 about 1 year 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 over 1 year ago Platform for implementing and verifying query compilers
SSProve 56 11 months ago Framework for modular cryptographic proofs based on the Mathematical Components library
VCFloat 24 over 1 year ago Framework for verifying C programs with floating-point computations
Verdi 595 over 1 year 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 about 1 year ago Interface for Coq based on the Vim text editor
Coq LSP 153 11 months 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 351 almost 3 years ago IDE extensions for Proof General's Coq mode
opam-switch-mode 5 over 2 years ago IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command
jsCoq 518 about 1 year ago Port of Coq to JavaScript, which enables running Coq projects in a browser
Jupyter kernel for Coq 94 about 1 year ago Coq support for the Jupyter Notebook web environment
VsCoq 349 11 months ago Language server and extension for the Visual Studio Code and VSCodium editors
VsCoq Legacy 349 11 months ago Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol
Waterproof editor 40 over 1 year ago Educational environment for writing mathematical proofs in interactive notebooks

Awesome Coq / Projects / Libraries
ALEA 25 about 4 years ago Library for reasoning on randomized algorithms
Algebra Tactics 33 11 months ago Ring and field tactics for Mathematical Components
Bignums 22 11 months ago Library of arbitrarily large numbers
Bedrock Bit Vectors 27 over 1 year ago Library for reasoning on fixed precision machine words
CertiGraph 17 11 months ago Library for reasoning about directed graphs and their embedding in separation logic
CoLoR 35 about 1 year ago Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library
coq-haskell 168 about 2 years ago Library smoothing the transition to Coq for Haskell users
Coq-Kruskal 0 11 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 43 about 1 year ago Library which provides a generic way to update Coq record fields
Coq-std++ Extended alternative standard library for Coq
ExtLib 129 11 months ago Collection of theories and plugins that may be useful in other Coq developments
FCSL-PCM 26 about 1 year 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 1 year ago Library of undecidable problems and reductions between them
Hahn 30 over 1 year ago Library for reasoning on lists and binary relations
Interaction Trees 206 about 1 year 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 year ago Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption
Mczify 24 11 months ago Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions
Metalib 73 over 1 year ago Library for programming language metatheory using locally nameless variable binding representations
Paco Library for parameterized coinduction
Regular Language Representations 41 over 1 year ago Translations between different definitions of regular languages, including regular expressions and automata
Relation Algebra 48 12 months ago Modular formalization of algebras with heterogeneous binary relations as models
Simple IO 31 11 months ago Input/output monad with user-definable primitive operations
TLC 38 11 months 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 34 11 months 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 191 11 months ago Curated collection of packages to support Coq use in industry, education, and research
coq-community Templates 13 11 months 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 11 months ago Docker images for many versions of Coq
Docker-MathComp 6 about 1 year 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 about 1 year ago Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator
Coinduction 15 about 1 year ago Plugin for doing proofs by enhanced coinduction
Coq-Elpi 141 11 months ago Extension framework based on λProlog providing an extensive API to implement commands and tactics
CoqHammer 220 11 months 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 11 months ago Function definition package for Coq
Gappa Tactic for discharging goals about floating-point arithmetic and round-off errors
Hierarchy Builder 97 11 months 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 396 11 months ago Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins
Mtac2 51 12 months ago Plugin adding typed tactics for backward reasoning
Paramcoq 45 about 1 year ago Plugin to generate parametricity translations of Coq terms
QuickChick 259 11 months ago Plugin for randomized property-based testing
SMTCoq 157 about 1 year 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 51 11 months ago Plugin that replaces the existing unification algorithm with an enhanced one
Waterproof proof language 33 12 months 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 3 years ago Coq implementation of Sokoban, the Japanese warehouse keepers' game
Hanoi 24 about 2 years ago The Tower of Hanoi puzzle in Coq, including generalizations and theorems about configurations
Mini-Rubik 4 over 2 years ago Coq formalization and solver of the 2x2x2 version of the Rubik's Cube puzzle
Name the Biggest Number 63 about 3 years ago Repository for submitting proven contenders for the title of biggest number in Coq
Natural Number Game 6 almost 3 years ago Coq version of the natural number game developed for the Lean prover
Sudoku 20 almost 3 years ago Formalization and solver of the Sudoku number-placement puzzle in Coq
T2048 22 about 2 years ago Coq version of the 2048 sliding tile game

Awesome Coq / Projects / Tools
Alectryon 237 11 months ago Collection of tools for writing technical documents that mix Coq code and prose
Autosubst 2 17 over 2 years 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 about 1 year ago Alternative HTML documentation generator for Coq
coqdoc Standard documentation tool that generates LaTeX or HTML files from Coq code
CoqOfOCaml 255 over 1 year ago Tool for generating idiomatic Coq from OCaml code
coq-dpdgraph 87 11 months ago Tool for building dependency graphs between Coq objects
coq-scripts 8 about 1 year ago Scripts for dealing with Coq files, including tabulating proof times
coq-tools 39 11 months ago Scripts for manipulating Coq developments

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

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

Awesome Coq / Projects / Type Theory and Mathematics
Analysis 210 11 months ago Library for classical real analysis compatible with Mathematical Components
Category Theory in Coq 759 11 months ago Axiom-free formalization of category theory
Completeness and Decidability of Modal Logic Calculi 8 about 1 year ago Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL
CoqPrime 37 about 1 year ago Library for certifying primality using Pocklington and Elliptic Curve certificates
CoRN 111 11 months ago Library of constructive real analysis and algebra
Coqtail Math 15 over 1 year 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 47 over 1 year ago Extension of Mathematical Components with finite maps, sets, and multisets
Four Color Theorem 174 12 months ago Formal proof of the Four Color Theorem, a landmark result of graph theory
Gaia 30 about 1 year ago Implementation of books from Bourbaki's Elements of Mathematics, including set theory and number theory
GeoCoq 186 over 1 year ago Formalization of geometry based on Tarski's axiom system
Graph Theory 35 11 months ago Formalized graph theory results
Homotopy Type Theory 1,262 11 months ago Development of homotopy-theoretic ideas
Infotheo 64 11 months 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 about 1 year ago Abstract interfaces for mathematical structures based on type classes
Monae 70 11 months ago Monadic effects and equational reasoning
Odd Order Theorem 27 about 1 year ago Formal proof of the Odd Order Theorem, a landmark result of finite group theory
Puiseuxth 4 about 1 year ago Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series
UniMath 964 11 months 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 5 years ago Verified hash-based approximate membership structures such as Bloom filters
CertiCoq 137 about 1 year ago Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language
Fiat-Crypto 723 11 months ago Cryptographic primitive code generation
Functional Algorithms Verified in SSReflect 45 12 months 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 275 11 months ago Formalized language and verified compiler for high-assurance and high-speed cryptography
JSCert 196 almost 2 years 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 110 about 1 year ago Definition of the RISC-V processor instruction set architecture and extensions
Stable sort algorithms in Coq 22 about 1 year ago Generic and modular proofs of correctness, including stability, of mergesort functions
Tarjan and Kosaraju 13 over 2 years 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 186 almost 2 years ago Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
WasmCert-Coq 100 12 months 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,883 11 months 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 over 1 year ago
Mathematical Components wiki 593 11 months ago
100 famous theorems proved using Coq 57 over 1 year 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 82 over 1 year ago Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming
Hydras & Co. 69 over 1 year 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 over 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 116 over 1 year ago Material on the Software Foundations series of textbooks, including a series of YouTube videos
MathComp School 6 almost 3 years ago Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library
Mechanized Semantics 64 over 1 year ago Companion Coq sources for a course on programming language semantics at Collège de France
Program Logics 40 over 4 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 114 over 1 year 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 12 months ago Demonstration of design patterns for programming and proving with canonical structures
MathComp Tutorial Materials 17 about 2 years ago Source code for Mathematical Components tutorials
Mike Nahas's Coq Tutorial Basics of using Coq to write formal proofs
Tricks in Coq 507 about 1 year ago Tips, tricks, and features in Coq that are hard to discover

Backlinks from these awesome lists:

More related projects: