Randomized Property-Based Testing Plugin for Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

Stdlib for the Rocq Prover

Visual Studio Code Extension and Language Server Protocol for Coq

A Visual Studio Code extension for Coq [maintainers=@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]

Coq plugin embedding elpi

A port of Coq to Javascript -- Run Coq in your Browser

A Seamless, Interactive Tactic Learner and Prover for Coq

Mathematical Components

The formal proof of the Odd Order Theorem

Formal proof of the Four Color Theorem

A library of mechanised undecidability proofs in the Coq proof assistant.

The CompCert formally-verified C compiler

Coq Enhancement Proposals

A plugin for Coq to add dependent pattern-matching.

Reflection library for Coq

Mirror repository for https://forge.ocamlcore.org/anonscm/git/lablgtk/lablgtk.git

Communication between Coq and SAT/SMT solvers

Cryptographic Primitive Code Generation by Fiat

An axiom-free formalization of category theory in Coq for personal study and practical work

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

A library of abstract interfaces for mathematical structures in Coq.

Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

Homotopy type theory