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. 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'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. coqffi - Automatically generates Coq FFI bindings to OCaml libraries. Coqtail - Library of mathematical theorems and tools proved inside the Coq proof assistant. 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. 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. Algebra Tactics - Experimental reflexive tactics for ring and field expressions. SSProve - Foundational framework for modular cryptographic proofs in Coq. PyCoq - Access Coq from Python. W-in-Coq - Coq formalization of Damas-Milner type system and its algorithm W.