UniMath - Coq library aims to formalize a substantial body of mathematics using the univalent point of view.
QuickChick - Randomized Property-Based Testing Plugin for Coq.
CoqHammer - Automated Reasoning Hammer Tool for Coq.
coq-ext-lib - Library of Coq definitions, theorems, and tactics.
Tricks in Coq - Some tips, tricks, and features in Coq that are hard to discover.
MetaCoq - Metaprogramming in Coq.
Fiat - Deductive Synthesis of Abstract Data Types in a Proof Assistant.
Equations - Function definition package for Coq.
Proofs - Selection of formal developments in Coq.
Programs and Proofs - Lecture notes for a short course on proving/programming in Coq via SSReflect.
CoqGym - Learning Environment for Theorem Proving with the Coq proof assistant.
Kami - DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness.
PeaCoq - Web-based front-end to the Coq proof assistant.
Kami - Platform for High-Level Parametric Hardware Specification and its Modular Verification.
coq-of-ocaml - Import OCaml programs to Coq.
Coq'Art - Coq code and exercises from the Coq'Art book.
GeoCoq - Formalization of geometry in Coq.
FreeSpec - Framework for implementing, certifying, and executing impure computations in Coq.
CoqPrime - Prime numbers for Coq.
coqffi - Automatically generates Coq FFI bindings to OCaml libraries.
Coqtail - Library of mathematical theorems and tools proved inside the Coq proof assistant.
Interaction Trees - Library for Representing Recursive and Impure Programs in Coq.
Alectryon - Library to process Coq snippets embedded in documents, showing goals and messages for each Coq sentence.
Cerise - Formalisation of a capability machine and principles for reasoning about security properties.
coq-procrastination - Small Coq library for collecting side conditions and deferring their proof.
Finite maps - Finite sets, finite maps, multisets and generic sets.
Alectryon - Collection of tools for writing technical documents that mix Coq code and prose.
Coq record update library - Automatically provides a generic way to update record fields.
HELIX - Formally verified operator language and rewriting engine for high-performance computing.
Bits - Formalization of bitset operations in Coq with a corresponding axiomatization and extraction to OCaml native integers.
Perennial - Verifying concurrent crash-safe systems.
Coq Platform - Multi platform setup for Coq, Coq libraries and tools.