Awesome Coq Awesome

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

Tools

Type Theory and Mathematics

Verified Software

Resources

Community

Blogs

Books

Tutorials and Hints