awesome-coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
307 stars
14 watching
19 forks
last commit: about 2 months ago
Linked from 2 awesome lists
awesomeawesome-listcoqresources
Awesome Coq / Projects / Frameworks | |||
| ConCert | 114 | 10 days ago | Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages |
| CoqEAL | 65 | about 2 months ago | Framework to ease change of data representations in proofs |
| FCF | 47 | 6 months ago | Framework for proofs of cryptography |
| Fiat | 147 | 19 days ago | Mostly automated synthesis of correct-by-construction programs |
| FreeSpec | 51 | 9 months ago | Framework for modularly verifying programs with effects and effect handlers |
| Hoare Type Theory | 69 | 12 days 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 | 55 | 3 months ago | Platform for implementing and verifying query compilers |
| SSProve | 57 | 30 days ago | Framework for modular cryptographic proofs based on the Mathematical Components library |
| VCFloat | 22 | 2 months ago | Framework for verifying C programs with floating-point computations |
| Verdi | 582 | 5 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 | 272 | 18 days ago | Interface for Coq based on the Vim text editor |
| Coq LSP | 145 | 11 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 | 351 | over 1 year ago | IDE extensions for Proof General's Coq mode |
| opam-switch-mode | 5 | about 1 year ago | IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command |
| jsCoq | 510 | 16 days ago | Port of Coq to JavaScript, which enables running Coq projects in a browser |
| Jupyter kernel for Coq | 93 | about 1 month ago | Coq support for the Jupyter Notebook web environment |
| VsCoq | 332 | 15 days ago | Language server and extension for the Visual Studio Code and VSCodium editors |
| VsCoq Legacy | 332 | 15 days ago | Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol |
| Waterproof editor | 38 | 7 months ago | Educational environment for writing mathematical proofs in interactive notebooks |
Awesome Coq / Projects / Libraries | |||
| ALEA | 25 | almost 3 years ago | Library for reasoning on randomized algorithms |
| Algebra Tactics | 32 | 24 days ago | Ring and field tactics for Mathematical Components |
| Bignums | 22 | 2 months ago | Library of arbitrarily large numbers |
| Bedrock Bit Vectors | 27 | 7 months ago | Library for reasoning on fixed precision machine words |
| CertiGraph | 17 | 4 months ago | Library for reasoning about directed graphs and their embedding in separation logic |
| CoLoR | 33 | 19 days ago | Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library |
| coq-haskell | 164 | 12 months ago | Library smoothing the transition to Coq for Haskell users |
| Coq-Kruskal | 0 | 4 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 | about 1 month ago | Library which provides a generic way to update Coq record fields |
| Coq-std++ | Extended alternative standard library for Coq | ||
| ExtLib | 128 | 18 days ago | Collection of theories and plugins that may be useful in other Coq developments |
| FCSL-PCM | 26 | 17 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 | 103 | 18 days ago | Library of undecidable problems and reductions between them |
| Hahn | 29 | 3 months ago | Library for reasoning on lists and binary relations |
| Interaction Trees | 199 | 6 months ago | Library for representing recursive and impure programs |
| LibHyps | 20 | 10 months 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 | 23 | 24 days ago | Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions |
| Metalib | 71 | 3 months ago | Library for programming language metatheory using locally nameless variable binding representations |
| Paco | Library for parameterized coinduction | ||
| Regular Language Representations | 42 | 3 months ago | Translations between different definitions of regular languages, including regular expressions and automata |
| Relation Algebra | 43 | 18 days ago | Modular formalization of algebras with heterogeneous binary relations as models |
| Simple IO | 30 | 17 days ago | Input/output monad with user-definable primitive operations |
| TLC | 37 | 6 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 | 32 | 12 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 | 189 | 19 days ago | Curated collection of packages to support Coq use in industry, education, and research |
| coq-community Templates | 13 | 15 days 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 | 25 days 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 | 19 days ago | Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator |
| Coinduction | 13 | 18 days ago | Plugin for doing proofs by enhanced coinduction |
| Coq-Elpi | 136 | 12 days ago | Extension framework based on λProlog providing an extensive API to implement commands and tactics |
| CoqHammer | 211 | 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 | 12 days ago | Function definition package for Coq |
| Gappa | Tactic for discharging goals about floating-point arithmetic and round-off errors | ||
| Hierarchy Builder | 96 | 15 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 | 370 | 9 days ago | Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins |
| Mtac2 | 51 | 24 days ago | Plugin adding typed tactics for backward reasoning |
| Paramcoq | 44 | 19 days ago | Plugin to generate parametricity translations of Coq terms |
| QuickChick | 249 | 16 days ago | Plugin for randomized property-based testing |
| SMTCoq | 155 | 16 days 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 | 4 months ago | Plugin that replaces the existing unification algorithm with an enhanced one |
| Waterproof proof language | 29 | 12 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 | over 1 year ago | Coq implementation of Sokoban, the Japanese warehouse keepers' game |
| Hanoi | 23 | 11 months 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 | 62 | about 2 years ago | Repository for submitting proven contenders for the title of biggest number in Coq |
| Natural Number Game | 6 | almost 2 years ago | Coq version of the natural number game developed for the Lean prover |
| Sudoku | 21 | almost 2 years ago | Formalization and solver of the Sudoku number-placement puzzle in Coq |
| T2048 | 22 | 11 months ago | Coq version of the 2048 sliding tile game |
Awesome Coq / Projects / Tools | |||
| Alectryon | 230 | 21 days ago | Collection of tools for writing technical documents that mix Coq code and prose |
| Autosubst 2 | 15 | 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 | about 1 month ago | Alternative HTML documentation generator for Coq |
| coqdoc | Standard documentation tool that generates LaTeX or HTML files from Coq code | ||
| CoqOfOCaml | 254 | 2 months ago | Tool for generating idiomatic Coq from OCaml code |
| coq-dpdgraph | 86 | 26 days ago | Tool for building dependency graphs between Coq objects |
| coq-scripts | 8 | 5 months ago | Scripts for dealing with Coq files, including tabulating proof times |
| coq-tools | 38 | 12 days ago | Scripts for manipulating Coq developments |
Awesome Coq / Projects / Tools / coq-tools | |||
| find-bug.py | 38 | 12 days ago | Automatically minimizes source files producing an error, creating small test cases for Coq bugs |
| absolutize-imports.py | 38 | 12 days ago | Processes source files to make loading of dependencies robust against shadowing of file names |
| inline-imports.py | 38 | 12 days ago | Creates stand-alone source files from developments by inlining the loading of all dependencies |
| minimize-requires.py | 38 | 12 days ago | Removes loading of unused dependencies |
| move-requires.py | 38 | 12 days ago | Moves all dependency loading statements to the top of source files |
| move-vernaculars.py | 38 | 12 days ago | Lifts many vernacular commands and inner lemmas out of proof script blocks |
| proof-using-helper.py | 38 | 12 days ago | Modifies source files to include proof annotations for faster parallel proving |
Awesome Coq / Projects / Tools | |||
| Cosette | 662 | almost 3 years ago | Automated solver for reasoning about SQL query equivalences |
| hs-to-coq | 77 | about 1 month ago | Converter from Haskell code to equivalent Coq code |
| lngen | 30 | 6 months ago | Tool for generating locally nameless Coq definitions and proofs |
| Menhir | Parser generator that can output Coq code for verified parsers | ||
| mCoq | 29 | almost 4 years ago | Mutation analysis tool for Coq projects |
| Ott | 343 | 14 days ago | Tool for writing definitions of programming languages and calculi that can be translated to Coq |
| PyCoq | 50 | over 2 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 | 587 | 12 days ago | Tool for specifying instruction set architecture (ISA) semantics of processors and generating Coq definitions |
| SerAPI | 128 | 26 days ago | Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions |
| Trakt | 14 | 8 months ago | Generic goal preprocessing tool for proof automation tactics |
Awesome Coq / Projects / Type Theory and Mathematics | |||
| Analysis | 197 | 11 days ago | Library for classical real analysis compatible with Mathematical Components |
| Category Theory in Coq | 746 | 17 days ago | Axiom-free formalization of category theory |
| Completeness and Decidability of Modal Logic Calculi | 8 | about 2 months ago | Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL |
| CoqPrime | 37 | 4 months ago | Library for certifying primality using Pocklington and Elliptic Curve certificates |
| CoRN | 108 | 19 days ago | Library of constructive real analysis and algebra |
| Coqtail Math | 15 | 3 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 | 4 months ago | Extension of Mathematical Components with finite maps, sets, and multisets |
| Four Color Theorem | 160 | 2 months ago | Formal proof of the Four Color Theorem, a landmark result of graph theory |
| Gaia | 28 | about 2 months ago | Implementation of books from Bourbaki's Elements of Mathematics, including set theory and number theory |
| GeoCoq | 180 | 4 months ago | Formalization of geometry based on Tarski's axiom system |
| Graph Theory | 32 | 3 months ago | Formalized graph theory results |
| Homotopy Type Theory | 1,246 | 6 days ago | Development of homotopy-theoretic ideas |
| Infotheo | 64 | 10 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 | 160 | 19 days ago | Abstract interfaces for mathematical structures based on type classes |
| Monae | 67 | about 2 months ago | Monadic effects and equational reasoning |
| Odd Order Theorem | 24 | about 2 months ago | Formal proof of the Odd Order Theorem, a landmark result of finite group theory |
| Puiseuxth | 4 | 11 days ago | Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series |
| UniMath | 954 | 13 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 | 122 | over 4 years ago | Verified hash-based approximate membership structures such as Bloom filters |
| CertiCoq | 135 | about 2 months ago | Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language |
| Fiat-Crypto | 707 | 12 days ago | Cryptographic primitive code generation |
| Functional Algorithms Verified in SSReflect | 42 | 15 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 | 250 | 11 days ago | Formalized language and verified compiler for high-assurance and high-speed cryptography |
| JSCert | 196 | 8 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 | 108 | about 2 months ago | Definition of the RISC-V processor instruction set architecture and extensions |
| Stable sort algorithms in Coq | 22 | 24 days ago | Generic and modular proofs of correctness, including stability, of mergesort functions |
| Tarjan and Kosaraju | 13 | about 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 | 182 | 10 months ago | Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework |
| WasmCert-Coq | 90 | 30 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,795 | 12 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 | 5 months ago | |
| Mathematical Components wiki | 575 | 16 days ago | |
| 100 famous theorems proved using Coq | 55 | 7 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 | 79 | 3 months ago | Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming |
| Hydras & Co. | 65 | 8 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 | 7 | over 1 year 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 | 109 | 5 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 | 62 | 6 months ago | Companion Coq sources for a course on programming language semantics at Collège de France |
| Program Logics | 37 | 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 | 109 | 2 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 | over 2 years ago | Demonstration of design patterns for programming and proving with canonical structures |
| MathComp Tutorial Materials | 17 | 11 months ago | Source code for Mathematical Components tutorials |
| Mike Nahas's Coq Tutorial | Basics of using Coq to write formal proofs | ||
| Tricks in Coq | 495 | about 2 months ago | Tips, tricks, and features in Coq that are hard to discover |
sindresorhus/awesome
0ex/more-awesome