β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'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. β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. β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. βcoq-bonsai - Generate a fresh bonsai in your terminal. Written in Coq. βCoq-Combi - Algebraic Combinatorics in Coq. βSniper - Coq plugin that provides a new Coq tactic, snipe, that provides general proof automation. βSMTCoq - Communication between Coq and SAT/SMT solvers. βTLC - Library for Classical Coq. βCertiCoq - Compiler for Gallina, the specification language of the Coq proof assistant. βTealeaves - Coq library for proving theorems about syntax abstractly. βHemiola - Coq framework to support structural design and proof of hardware cache-coherence protocols. βMczify - Micromega tactics for Mathematical Components. βHierarchy Builder - High level commands to declare a hierarchy based on packed classes. βCoq Package Index - Archive for all Coq related OPAM packages organized in various repositories. (Code) βSemantics - Survey of semantics styles in Coq. βAAC Tactics - Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators. βVermillion - LL(1) parser generator verified in Coq. βCoq-Elpi - Coq plugin embedding Elpi. βApery - Formal proof of the irrationality of zeta(3), the ApΓ©ry constant. βcoq-ext-lib - Collection of theories and plugins that may be useful in other Coq developments. βMath Classes - Library of abstract interfaces for mathematical structures in Coq. βC-CoRN - Coq Repository at Nijmegen. βch2o - Aims at formalizing novel features of the ISO C11 standard of the C programming language. βATBR - Coq library and tactic for deciding Kleene algebras.