Rocq-community

All

77 repositories

run-coq-bug-minimizer
Public
Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
Shell
•
MIT License
•0•2•10•0•Updated Jan 30, 2026Jan 30, 2026
coq-nix-toolbox
Public
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
nix coq
Nix
•
MIT License
•21•50•31•7•Updated Jan 30, 2026Jan 30, 2026
apery
Public
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
coq ssreflect mathcomp
Rocq Prover
•
Other
•8•25•5•0•Updated Jan 27, 2026Jan 27, 2026
coq-dpdgraph
Public
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
dependency-analysis coq dependency-graph docker-coq-action coq-ci coq-platform
OCaml
•
GNU Lesser General Public License v2.1
•34•97•14•12•Updated Jan 26, 2026Jan 26, 2026
rocq-lsp
Public
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]
ide coq language-server-protocol vscode-extension user-interface interactive-theorem-proving rocq rocq-prover
OCaml
•
GNU Lesser General Public License v2.1
•51•196•140•5•Updated Jan 25, 2026Jan 25, 2026
trocq
Public
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx,@MysaaJava]
coq parametricity
Rocq Prover
•
GNU Lesser General Public License v3.0
•10•27•17•4•Updated Jan 23, 2026Jan 23, 2026
coqeal
Public
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
coq refinement mathcomp coq-ci coq-platform mathcomp-ci
Rocq Prover
•
Other
•17•74•6•3•Updated Jan 20, 2026Jan 20, 2026
micromega-plugin
Public
The Rocq Micromega plugin [maintainers=@fajb,@proux01]
OCaml
•
GNU Lesser General Public License v2.1
•0•0•0•0•Updated Jan 13, 2026Jan 13, 2026
rocq-lean-import
Public
OCaml
•
GNU Lesser General Public License v2.1
•11•26•9•0•Updated Jan 9, 2026Jan 9, 2026
corn
Public
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
coq coq-library real-number coq-ci coq-platform
Rocq Prover
•
GNU General Public License v2.0
•46•115•7•1•Updated Jan 9, 2026Jan 9, 2026
math-classes
Public
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
coq mathematics typeclasses coq-library coq-ci coq-platform
Rocq Prover
•
MIT License
•43•168•11•1•Updated Jan 9, 2026Jan 9, 2026
bignums
Public
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
large-numbers coq coq-plugin docker-coq-action coq-ci coq-platform
Rocq Prover
•
GNU Lesser General Public License v2.1
•23•25•1•1•Updated Jan 9, 2026Jan 9, 2026
paramcoq
Public
Old Coq plugin for parametricity [maintainer=@ppedrot]
coq coq-plugin parametricity docker-coq-action coq-ci coq-platform
Rocq Prover
•
Other
•29•44•8•1•Updated Jan 8, 2026Jan 8, 2026
coq-performance-tests
Public
A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]
testing performance coq
Coq
•
MIT License
•7•8•1•5•Updated Dec 15, 2025Dec 15, 2025
semantics
Public
A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [m…
coq programming-language-semantics
Rocq Prover
•
MIT License
•5•57•1•0•Updated Nov 28, 2025Nov 28, 2025
coq-100-theorems
Public
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
coq theorems
HTML
•
Other
•15•61•2•2•Updated Nov 26, 2025Nov 26, 2025
awesome-coq
Public
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
awesome coq resources awesome-list
Creative Commons Zero v1.0 Universal
•25•375•7•1•Updated Nov 5, 2025Nov 5, 2025
huffman
Public
Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
ocaml coq huffman-coding huffman-tree coq-extraction docker-coq-action coq-nix-toolbox
Rocq Prover
•
Other
•4•13•0•1•Updated Oct 31, 2025Oct 31, 2025
templates
Public
Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@liyishuai,@palmskog,@Zimmi48]
continuous-integration coq mustache-templates
Mustache
•
The Unlicense
•10•16•23•4•Updated Oct 30, 2025Oct 30, 2025
graph-theory
Public
Graph Theory [maintainers=@chdoc,@damien-pous]
coq graph-theory mathcomp docker-coq-action mathcomp-ci
Rocq Prover
•4•41•2•1•Updated Oct 30, 2025Oct 30, 2025
aac-tactics
Public
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
coq coq-plugin coq-tactic docker-coq-action nix-action coq-ci coq-platform
OCaml
•
Other
•24•36•3•4•Updated Oct 28, 2025Oct 28, 2025
coqdocjs
Public
Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]
javascript css html coq coqdoc
JavaScript
•
BSD 2-Clause "Simplified" License
•20•40•4•1•Updated Oct 21, 2025Oct 21, 2025
coqtail-math
Public
Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis…
coq complex-analysis real-analysis
Rocq Prover
•
Other
•0•16•0•0•Updated Oct 20, 2025Oct 20, 2025
docker-rocq
Public
Docker images of the Rocq Prover (see also: https://github.com/rocq-community/docker-coq-action) [maintainer=@Justme0606]
Dockerfile
•
MIT License
•0•2•5•0•Updated Oct 17, 2025Oct 17, 2025
tarjan
Public
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintain…
coq tarjan-algorithm ssreflect mathcomp mathcomp-ci
Rocq Prover
•
Other
•8•18•0•0•Updated Oct 14, 2025Oct 14, 2025
fourcolor
Public
Formal proof of the Four Color Theorem [maintainer=@ybertot]
coq ssreflect four-color-theorem mathcomp coq-ci
Rocq Prover
•
Other
•23•226•0•1•Updated Oct 14, 2025Oct 14, 2025
fav-ssr
Public
Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
avl-tree coq huffman-coding quadtree binomial-heap ssreflect 2-3-tree leftist-heap mathcomp redblack-tree
Rocq Prover
•
MIT License
•7•50•13•2•Updated Oct 8, 2025Oct 8, 2025
reduction-effects
Public
A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
coq side-effects coq-plugin coq-ci
Makefile
•
Mozilla Public License 2.0
•7•7•4•0•Updated Oct 3, 2025Oct 3, 2025
coq-ext-lib
Public
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
library programming coq coq-ci coq-platform
Rocq Prover
•
BSD 2-Clause "Simplified" License
•52•137•18•3•Updated Oct 2, 2025Oct 2, 2025
bits
Public
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
bitset coq coq-library ssreflect paper-artifacts coq-extraction mathcomp
Rocq Prover
•
Apache License 2.0
•7•24•4•0•Updated Sep 7, 2025Sep 7, 2025