UniMath - Coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Mathematical Components - Libraries of formalized mathematics developed using the Coq proof assistant. (GitHub)

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.

Formal Reasoning About Programs - In-progress, open-source book by Adam Chlipala simultaneously introducing the Coq proof assistant and techniques for proving correctness of programs. (HN) (Web) (MIT course)

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.