Rocq-community

About

Rocq-community is a project for a collaborative, community-driven effort for the long-term maintenance and advertisement of packages for the Rocq Prover. The organization is run by volunteer Rocq users. Everyone is welcome - you don’t need to be a very experienced Rocq user to participate. See the contributing guide for more information on how to get involved.

Project Hosting

Repositories for Rocq-related projects can be hosted in the Rocq-community organization on GitHub whenever any of the following is the case:

the project has become a collective work (several community members are actively working on it);
the initial author has stopped maintaining the project and someone else is volunteering to do so;
the initial author is still maintaining the project but they want to encourage other community members to participate in the maintenance and possibly take over (and the project is indeed raising interest from the community);
the project is a library or tool of general interest and it makes sense to develop it collaboratively.

Once a project has joined Rocq-community, community members collaborate to ensure:

project package definitions are continuously published in Rocq’s opam package index and other relevant venues;
projects use best practices for automation (e.g., building and continuous integration) as the project and Rocq itself evolves;
projects provide rich metadata and documentation to enable application in other projects and in research.

More details can be found in the Rocq-community manifesto, in particular on the process for proposing a new package.

Contact

Chat with us on Zulip
Volunteer and contribute on GitHub
Discuss with us on Rocq’s Discourse forum

Current Projects

Below is a categorized list of active projects currently hosted in Rocq-community. A star ⭐ indicates that the project is recommended for (re)use, while a warning sign ⚠️ indicates that the project is experimental or for other reasons not currently recommended for (re)use. Independently of stars or warnings, a bird of prey 🦅 indicates that a project is part of the Rocq Platform, a distribution of the Rocq Prover together with many generally useful libraries, plugins and tools.

Automation

Coq Nix Toolbox - Nix helper scripts to automate local builds and CI for Rocq.
coq-performance-tests ⚠️ - Library of source files for testing Rocq performance regressions.
coq-performance-tests-plots-history ⚠️ - Repository with plot history for Rocq performance tests.
Docker-Base - Parent image for Docker images of the Rocq Prover and the Coq proof assistant.
Docker-Coq ⭐ - Docker images of the Coq proof assistant.
Docker-Coq-Action ⭐ - GitHub Action using Docker-Coq and Docker-Rocq.
Docker-Rocq ⭐ - Docker images of the Rocq Prover.
run-coq-bug-minimizer ⚠️ - Repository for triggering runs of the Rocq bug minimizer using GitHub Actions.
Templates - Templates for configuration files and scripts useful for maintaining Rocq projects.

Documentation and Tutorials

100 famous theorems proved using Coq - Repository tracking the theorems that have been proved in Rocq from a list of 100 famous theorems.
Awesome Coq ⭐ - Curated list of awesome Rocq libraries, plugins, tools, verification projects, and resources.
Coq’Art - Rocq code and exercises from the Coq’Art book.
Coq Plugin Template - Template repository for writing Rocq plugins using the Dune build system, showcasing some advanced features such as linking to an external library.
Coq Program Verification Template - Template repository for program verification in Rocq, showcasing reasoning on CompCert’s Clight language using the Verified Software Toolchain.
Hoare Tutorial - Tutorial on reflecting in Rocq the generation of Hoare proof obligations.
Hydras & Co. ⭐ - Variations on Kirby and Paris’ hydra battles and other entertaining math in Rocq, including the Gödel-Rosser 1st incompleteness theorem (collaborative, documented, includes exercises).
Lemma Overloading - Libraries demonstrating design patterns for programming and proving with canonical structures in Rocq.
Rosetta stone of metaprogramming in Coq - Different examples of tactics, plugins, etc., implemented in different metaprogramming languages.
Semantics - Survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation.
Tricks in Coq ⭐ - Tips, tricks, and features in Rocq that are hard to discover, including example code.

Interfaces

Conceal for VSCode - Prettify symbols mode for the Visual Studio Code and VSCodium editors.
coqdocjs - Collection of scripts to improve the HTML output of rocqdoc.
VsCoq Legacy - Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Rocq’s legacy XML protocol.

Libraries

ALEA - Rocq library for reasoning on randomized algorithms.
Almost Full ⚠️ - Rocq development of almost-full relations, including the Ramsey Theorem, useful for proving termination.
Autosubst - Rocq library and tactics for parallel de Bruijn substitutions.
Bits ⚠️ - Formalization of bitset operations in Rocq and the corresponding axiomatization and extraction to OCaml native integers.
CoqEAL 🦅 - Framework to ease change of data representations in proofs.
Coq ExtLib ⭐ 🦅 - Library of Rocq definitions, theorems, and tactics.
Dblib - Rocq library for working with de Bruijn indices.
Generic Environments - Library which provides an abstract data type of environments.
Parseque - Total parser combinators library, port of agdarsec.
RegLang ⭐ 🦅 - Regular language representations in Rocq.

Plugins

AAC Tactics ⭐ 🦅 - Rocq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.
ATBR - Rocq library and plugin tactic for deciding Kleene algebras.
Bignums ⭐ 🦅 - Rocq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library.
coq-dpdpgraph 🦅 - Plugin and tools for obtaining dependencies between Rocq objects (definitions, theorems) and produce graphs.
Paramcoq 🦅 - Rocq plugin for parametricity.
Reduction Effects ⚠️ 🦅 - Plugin to add side effects to some Rocq reduction strategies.
Trocq ⚠️ - Modular parametricity plugin for proof transfer using univalence.

Tools

coqffi - Tool for generating Rocq FFI bindings to OCaml libraries.
Proviola ⚠️ - Tool for reanimation of Rocq proofs.

Type Theory and Mathematics

Apery - Proof in Rocq, by computer algebra, that the real number ζ(3), known as Apéry’s constant, is irrational.
Binary Rational Numbers - Rocq development of rational numbers as finite binary lists.
Completeness and Decidability of Modal Logic Calculi - Constructive proofs of soundness and completeness for the modal logics K, K*, CTL, PDL, and PDL with converse.
CoRN ⭐ 🦅 - Repository of constructive mathematics formalized in Rocq, including the algebraic hierarchy and real calculus.
Coqtail - Library of mathematical theorems and tools in Rocq, ranging from arithmetic to real and complex analysis.
Dedekind Reals - Formalization of the Dedekind real numbers in Rocq.
Exact real arithmetic ⚠️ - Exact real arithmetic in Rocq.
Four Color Theorem ⭐ - Formal proof in Rocq of the Four Color Theorem, a landmark result in graph theory.
Gaia ⭐ - Implementation of books from Bourbaki’s Elements of Mathematics in Rocq.
Graph Theory - Library of formalized graph theory results in Rocq.
High School Geometry - Geometry in Rocq for French high school.
Math Classes ⭐ 🦅 - Library of abstract interfaces for mathematical structures in Rocq.
Pocklington - Pocklington’s criterion for primality in Rocq.
Topology - General topology and set theory in Rocq.

Verified Software

Bertrand - Rocq proof of Bertrand’s postulate on existence of primes, with an application to the correctness of Knuth’s algorithm for prime numbers.
Buchberger - Verified implementation of Buchberger’s algorithm for computing Gröbner bases in Rocq.
Coqoban - Rocq implementation of Sokoban, the Japanese warehouse keepers’ game.
Chapar ⚠️ - Framework for verification of causal consistency for distributed key-value stores and their clients in Rocq.
Huffman ⭐ - Correctness proof of the Huffman coding algorithm in Rocq.
JMLCoq ⚠️ - Rocq definition of JML and a verified runtime assertion checker.
Modular Finite Maps over Ordered Types - Several implementations of finite maps over arbitrary ordered types using Rocq functors, including using red-black trees and AVL trees.
Regexp Brzozowski ⚠️ - Decision procedures in Rocq for regular expression equivalence.
Stalmarck - Verified implementation in Rocq of Stålmarck’s algorithm for proving tautologies.
Sudoku - Certified Sudoku solver in Rocq.
Tarjan and Kosaraju - Rocq formalizations of algorithms originally due to Kosaraju and Tarjan for finding strongly connected components in finite graphs.