Awesome Coq
A curated list of awesome Coq libraries, plugins, tools, and resources.
The Coq proof assistant provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs.
Contributions welcome! Read the contribution guidelines first.
Contents
- Projects
- Frameworks
- User Interfaces
- Libraries
- Package and Build Management
- Plugins
- Puzzles and Games
- Tools
- Type Theory and Mathematics
- Verified Software
- Resources
- Community
- Blogs
- Books
- Course Material
- Tutorials and Hints
Projects
Frameworks
- ConCert - Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages.
- CoqEAL - Framework to ease change of data representations in proofs.
- FCF - Framework for proofs of cryptography.
- Fiat - Mostly automated synthesis of correct-by-construction programs.
- FreeSpec - Framework for modularly verifying programs with effects and effect handlers.
- Hoare Type Theory - 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 - Platform for implementing and verifying query compilers.
- SSProve - Framework for modular cryptographic proofs based on the Mathematical Components library.
- VCFloat - Framework for verifying C programs with floating-point computations.
- Verdi - 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.
User Interfaces
- CoqIDE - Standalone graphical tool for interacting with Coq.
- Coqtail - Interface for Coq based on the Vim text editor.
- Coq LSP - 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 - IDE extensions for Proof General's Coq mode.
- opam-switch-mode - IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command.
- jsCoq - Port of Coq to JavaScript, which enables running Coq projects in a browser.
- Jupyter kernel for Coq - Coq support for the Jupyter Notebook web environment.
- VsCoq - Language server and extension for the Visual Studio Code and VSCodium editors.
- VsCoq Legacy - Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol.
- Waterproof editor - Educational environment for writing mathematical proofs in interactive notebooks.
- Tree Sitter Rocq - Partial Rocq tree-sitter grammar useful for syntax highlighting in text editors like Helix, but not recommended for full parsing of Rocq code.
Libraries
- ALEA - Library for reasoning on randomized algorithms.
- Algebra Tactics - Ring and field tactics for Mathematical Components.
- Bignums - Library of arbitrarily large numbers.