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: 5 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 2 months ago Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages
CoqEAL 67 about 1 month ago Framework to ease change of data representations in proofs
FCF 48 9 months ago Framework for proofs of cryptography
Fiat 149 about 2 months ago Mostly automated synthesis of correct-by-construction programs
FreeSpec 52 about 1 year ago Framework for modularly verifying programs with effects and effect handlers
Hoare Type Theory 70 3 months 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 6 months ago Platform for implementing and verifying query compilers
SSProve 56 about 2 months ago Framework for modular cryptographic proofs based on the Mathematical Components library
VCFloat 24 6 months ago Framework for verifying C programs with floating-point computations
Verdi 595 8 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 4 months ago Interface for Coq based on the Vim text editor
Coq LSP 153 about 1 month 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 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 518 3 months ago Port of Coq to JavaScript, which enables running Coq projects in a browser
Jupyter kernel for Coq 94 5 months ago Coq support for the Jupyter Notebook web environment
VsCoq 349 about 1 month ago Language server and extension for the Visual Studio Code and VSCodium editors
VsCoq Legacy 349 about 1 month ago Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol
Waterproof editor 40 10 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 33 about 1 month ago Ring and field tactics for Mathematical Components
Bignums 22 about 1 month ago Library of arbitrarily large numbers
Bedrock Bit Vectors 27 11 months ago Library for reasoning on fixed precision machine words
CertiGraph 17 about 1 month ago Library for reasoning about directed graphs and their embedding in separation logic
CoLoR 35 3 months ago Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library
coq-haskell 168 over 1 year ago Library smoothing the transition to Coq for Haskell users
Coq-Kruskal 0 about 1 month 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 5 months ago Library which provides a generic way to update Coq record fields
Coq-std++ Extended alternative standard library for Coq
ExtLib 129 about 1 month ago Collection of theories and plugins that may be useful in other Coq developments
FCSL-PCM 26 3 months 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 4 months ago Library of undecidable problems and reductions between them
Hahn 30 7 months ago Library for reasoning on lists and binary relations
Interaction Trees 206 3 months ago Library for representing recursive and impure programs
LibHyps 20 about 1 month ago Library of Ltac tactics to manage and manipulate hypotheses in proofs
MathComp Extra 5 3 months ago Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption
Mczify 24 about 1 month ago Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions
Metalib 73 7 months ago Library for programming language metatheory using locally nameless variable binding representations
Paco Library for parameterized coinduction
Regular Language Representations 41 6 months ago Translations between different definitions of regular languages, including regular expressions and automata
Relation Algebra 48 2 months ago Modular formalization of algebras with heterogeneous binary relations as models
Simple IO 31 about 1 month ago Input/output monad with user-definable primitive operations
TLC 38 about 1 month 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 about 1 month 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 about 1 month 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 about 1 month ago Docker images for many versions of Coq
Docker-MathComp 6 3 months 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 3 months ago Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator
Coinduction 15 4 months ago Plugin for doing proofs by enhanced coinduction
Coq-Elpi 141 about 1 month ago Extension framework based on λProlog providing an extensive API to implement commands and tactics
CoqHammer 220 about 2 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 about 1 month ago Function definition package for Coq
Gappa Tactic for discharging goals about floating-point arithmetic and round-off errors
Hierarchy Builder 97 about 1 month 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 about 1 month ago Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins
Mtac2 51 about 2 months ago Plugin adding typed tactics for backward reasoning
Paramcoq 45 4 months ago Plugin to generate parametricity translations of Coq terms
QuickChick 259 about 1 month ago Plugin for randomized property-based testing
SMTCoq 157 4 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 51 about 1 month ago Plugin that replaces the existing unification algorithm with an enhanced one
Waterproof proof language 33 2 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 about 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 over 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 237 about 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 5 months ago Alternative HTML documentation generator for Coq
coqdoc Standard documentation tool that generates LaTeX or HTML files from Coq code
CoqOfOCaml 255 6 months ago Tool for generating idiomatic Coq from OCaml code
coq-dpdgraph 87 about 1 month ago Tool for building dependency graphs between Coq objects
coq-scripts 8 3 months ago Scripts for dealing with Coq files, including tabulating proof times
coq-tools 39 about 1 month ago Scripts for manipulating Coq developments

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

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

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

Backlinks from these awesome lists:

More related projects: