awesome-coq
github.com/rocq-community/awesome-coq ↗A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
Use this list with your AI agent
Add the Context Awesome MCP server to Claude, Cursor, or any MCP client, then ask:
"Show me community resources from awesome-coq"
Installation instructions →What's inside
Resources
- 100 famous theorems proved using CoqCommunity
- An Introduction to MathComp-AnalysisCourse Material
Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis.
- Certified Programming with Dependent TypesBooks
Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
- Computer Arithmetic and Formal ProofsBooks
Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.
- Coq'ArtBooks
The first book dedicated to Coq.
- Coq'Art Exercises and TutorialsTutorials and Hints
Coq code and exercises from the Coq'Art book, including additional tutorials.
Projects
- AAC TacticsPlugins
Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.
- ALEALibraries
Library for reasoning on randomized algorithms.
- AlectryonTools
Collection of tools for writing technical documents that mix Coq code and prose.
- Algebra TacticsLibraries
Ring and field tactics for Mathematical Components.
- AnalysisType Theory and Mathematics
Library for classical real analysis compatible with Mathematical Components.
- Autosubst-ocamlTools
Tool that generates Coq code for handling binders in syntax, such as for renaming and substitutions.
Showing a sample of 208 resources. View the full list on GitHub →