104 packages · page 1 of 2
| Package ▲ | Version | Maintainers | # | Teams | Deps | Used by | Used by (transitive) | Status |
|---|---|---|---|---|---|---|---|---|
CakeML backend for Peregrine |
0.1.0 |
1 | 7 | 0 | 0 | single | ||
CertiRocq |
0.9.1+9.1 |
2 | 9 | 0 | 0 | maintained | ||
20230107 |
0 | 5 | 0 | 0 | unmaintained | |||
CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant |
1.8.6 |
2 | 5 | 0 | 0 | maintained | ||
A framework for smart contract verification in Rocq |
1.0.1 |
1 | 9 | 0 | 0 | single | ||
Collection of theories and plugins that may be useful in other Coq developments |
0.13.2 |
2 | 5 | 18 | 30 | maintained | ||
Library for Representing Recursive and Impure Programs in Coq |
5.2.1 |
1 | 6 | 2 | 2 | single | ||
20230107 |
0 | 5 | 0 | 0 | unmaintained | |||
Support library for verified Coq parsers produced by Menhir |
20260203 |
1 | 5 | 2 | 5 | single | ||
Ordinal Numbers in Coq |
0.5.6 |
1 | 5 | 0 | 0 | single | ||
Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck |
2.1.1 |
1 | 8 | 1 | 1 | single | ||
20230107 |
0 | 5 | 1 | 1 | unmaintained | |||
A framework for extracting Rocq programs to Rust and Elm |
0.2.1 |
1 | 7 | 1 | 1 | single | ||
A framework for extracting Rocq programs to Rust and Elm |
0.2.1 |
1 | 6 | 2 | 5 | single | ||
A framework for extracting Rocq programs to Rust and Elm |
0.2.1 |
1 | 7 | 1 | 3 | single | ||
A framework for extracting Rocq programs to Rust and Elm |
0.2.1 |
1 | 8 | 1 | 2 | single | ||
A framework for extracting Rocq programs to Rust and Elm |
0.2.1 |
1 | 7 | 1 | 3 | single | ||
Verified Software Toolchain |
2.17 |
0 | 6 | 0 | 0 | unmaintained | ||
Coq plugin providing tactics for rewriting universally quantified equations |
9.0.0 |
1 | 5 | 1 | 1 | single | ||
Automation for de Bruijn syntax and substitution in Coq |
1.9 |
2 | 6 | 0 | 0 | maintained | ||
9.0.0+rocq9.1 |
0 | 5 | 8 | 9 | unmaintained | |||
Library for serialization to S-expressions |
0.4.1 |
1 | 6 | 1 | 2 | single | ||
Library for serialization via S-expressions using bytestrings. Alternative to coq-ceres which uses String from standard library. |
1.0.0 |
1 | 7 | 2 | 2 | single | ||
Formally verified C compiler |
3.18 |
3 | 9 | 3 | 3 | maintained unfree | ||
Rocq plugin embedding ELPI |
3.5.0 |
1 | 5 | 2 | 46 | single | ||
General-purpose automated reasoning hammer tool for Coq |
1.3.3+9.1 |
1 | 5 | 0 | 0 | single | ||
Reconstruction tactics for the hammer for Coq |
1.3.3+9.1 |
1 | 5 | 1 | 1 | single | ||
Language Server Protocol and VS Code Extension for Coq |
0.2.5+9.1 |
1 | 6 | 0 | 0 | single | ||
Library to create Coq record update functions |
0.3.6 |
1 | 4 | 0 | 0 | single | ||
CoqEAL - The Coq Effective Algebra Library |
2.1.2 |
0 | 8 | 1 | 1 | unmaintained | ||
Library to certify primality using Pocklington certificate and Elliptic Curve Certificate |
8.20 |
1 | 5 | 0 | 0 | single | ||
Coq library for Reals |
3.4.5 |
1 | 7 | 2 | 4 | single | ||
Coq library for tactics, basic definitions, sets, maps |
0.0.7 |
1 | 6 | 0 | 0 | single | ||
Generic instances of MathComp classes |
0.2.3 |
1 | 6 | 2 | 2 | single | ||
Build dependency graphs between Coq objects |
1.0+9.1 |
1 | 4 | 0 | 0 | single | ||
Plugin for Coq to add dependent pattern-matching |
1.3.1+9.1 → 1.3+8.19 |
1 | 6 | 15 | 23 | single outdated | ||
Finite data structures with extensional reasoning |
0.5.0 |
1 | 6 | 1 | 1 | single | ||
Coq library of Partial Commutative Monoids |
2.2.0 |
1 | 6 | 0 | 0 | single | ||
Floating-point formalization for the Rocq system |
4.2.2 |
1 | 7 | 5 | 8 | single | ||
Formal proof of the Four Color Theorem |
1.4.3 |
1 | 7 | 1 | 1 | single | ||
Implementation of books from Bourbaki's Elements of Mathematics in Coq |
2.4 |
1 | 8 | 0 | 0 | single | ||
Library of formalized graph theory results in Coq |
0.9.7 |
1 | 10 | 0 | 0 | single | ||
High level commands to declare a hierarchy based on packed classes |
1.10.3 |
2 | 5 | 15 | 45 | maintained | ||
Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant |
4.11.5 |
1 | 11 | 3 | 3 | single | ||
Rocq development of the Iris Project |
4.5.0 |
2 | 5 | 0 | 0 | maintained | ||
Jasmin language & verified compiler |
2026.03.3 |
2 | 7 | 0 | 0 | maintained | ||
From JSON to Coq, and vice versa |
0.2.0 |
0 | 7 | 0 | 0 | unmaintained | ||
ValidSDP |
1.1.1 |
0 | 10 | 1 | 1 | unmaintained | ||
Library of abstract interfaces for mathematical structures in Coq |
9.2.0 |
2 | 5 | 0 | 0 | maintained | ||
2.5.0 |
3 | 7 | 0 | 0 | maintained | |||
2.5.0 |
3 | 8 | 11 | 26 | maintained | |||
Ring and field tactics for Mathematical Components |
1.2.7 |
1 | 8 | 3 | 3 | single | ||
Analysis library compatible with Mathematical Components |
1.16.0 |
1 | 9 | 3 | 4 | single | ||
Analysis library compatible with Mathematical Components |
1.16.0 |
1 | 8 | 1 | 1 | single | ||
Small library to do epsilon - N reasonning |
1.0.4 |
0 | 5 | 4 | 9 | unmaintained | ||
2.5.0 |
3 | 6 | 17 | 44 | maintained | |||
2.5.0 |
3 | 7 | 2 | 2 | maintained | |||
Analysis library compatible with Mathematical Components |
1.16.0 |
1 | 7 | 1 | 9 | single | ||
Analysis library compatible with Mathematical Components |
1.16.0 |
1 | 7 | 1 | 1 | single | ||
2.5.0 |
3 | 7 | 5 | 12 | maintained | |||
2.5.0 |
3 | 7 | 9 | 29 | maintained | |||
Finset and finmap library |
2.2.2 |
0 | 5 | 3 | 13 | unmaintained | ||
Coq formalization of information theory and linear error-correcting codes |
0.9.7 |
0 | 7 | 0 | 0 | unmaintained | ||
2.5.0 |
3 | 7 | 2 | 32 | maintained | |||
Mathematical Components Library on real closed fields |
2.0.5 |
0 | 6 | 2 | 7 | unmaintained | ||
Analysis library compatible with Mathematical Components |
1.16.0 |
1 | 6 | 2 | 8 | single | ||
Analysis library compatible with Mathematical Components |
1.16.0 |
1 | 7 | 3 | 4 | single | ||
2.5.0 |
3 | 7 | 1 | 13 | maintained | |||
Proofs of Tarjan and Kosaraju connected components algorithms |
1.0.5 |
0 | 6 | 0 | 0 | unmaintained | ||
Yet Another Coq Library on Machine Words |
3.5 |
1 | 9 | 2 | 2 | single | ||
Micromega tactics for Mathematical Components |
1.7.0+2.4+9.0 |
1 | 8 | 1 | 4 | single | ||
1.5.1-9.1 |
1 | 11 | 0 | 0 | single | |||
1.5.1-9.1 |
1 | 8 | 2 | 19 | single | |||
1.5.1-9.1 |
1 | 10 | 7 | 11 | single | |||
1.5.1-9.1 |
1 | 10 | 4 | 4 | single | |||
1.5.1-9.1 |
1 | 8 | 3 | 16 | single | |||
1.5.1-9.1 |
1 | 10 | 1 | 1 | single | |||
1.5.1-9.1 |
1 | 8 | 2 | 13 | single | |||
1.5.1-9.1 |
1 | 10 | 2 | 2 | single | |||
1.5.1-9.1 |
1 | 9 | 4 | 14 | single | |||
1.5.1-9.1 |
1 | 8 | 6 | 16 | single | |||
1.5.1-9.1 |
1 | 8 | 1 | 1 | single | |||
1.5.1-9.1 |
1 | 7 | 2 | 21 | single | |||
Plugin for (semi)decision procedures for arithmetic. |
1.1.1 |
0 | 5 | 0 | 0 | unmaintained | ||
Typed tactic language for Coq |
1.4-rocq9.1 |
0 | 6 | 0 | 0 | unmaintained | ||
Coq/SSReflect Library for Monoidal Rings and Multinomials |
2.4.0 |
0 | 9 | 2 | 2 | unmaintained | ||
Formal proof of the Odd Order Theorem |
2.4.0 |
1 | 5 | 0 | 0 | single | ||
Coq library implementing parameterized coinduction |
4.2.3 |
2 | 5 | 1 | 3 | maintained | ||
Library for serialization to S-expressions |
0.2.0 |
1 | 7 | 1 | 1 | single | ||
Total parser combinators in Rocq |
0.3.1 |
1 | 5 | 1 | 2 | single | ||
Regular Language Representations in Coq |
1.2.2 |
1 | 6 | 0 | 0 | single | ||
Relation algebra library for Rocq |
1.8.1 |
1 | 7 | 0 | 0 | single | ||
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography |
0.0.15 |
0 | 5 | 0 | 0 | unmaintained | ||
Rocqnavi: an HTML documentation generator for Rocq prover |
0.5.0 |
1 | 4 | 0 | 0 | single | ||
Purely functional IO for Coq |
1.11.0 |
1 | 6 | 1 | 2 | single | ||
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq |
0.3.1 |
1 | 11 | 0 | 0 | single | ||
2.5.0 |
3 | 8 | 5 | 10 | maintained | |||
Rocq Proof Assistant -- Standard Library |
9.0.0 |
0 | 4 | 47 | 74 | unmaintained | ||
Extended “Standard Library” for Rocq |
1.13.0 |
2 | 5 | 2 | 2 | maintained | ||
Enhanced unification algorithm for Coq |
1.6-9.1 |
0 | 4 | 1 | 1 | unmaintained |