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…

Language Server Protocol and VS Code Extension for Coq

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting

Coq plugin for parametricity [maintainer=@proux01]

Coq plugin embedding elpi

A plugin for Coq to add dependent pattern-matching.

Metaprogramming in Coq

Krivine's classical realizability

Randomized Property-Based Testing Plugin for Coq

IO for Gallina

Communication between Coq and SAT/SMT solvers

The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to…

A Seamless, Interactive Tactic Learner and Prover for Coq

The Rocq Micromega plugin [maintainers=@fajb,@proux01]

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.

Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]

Cryptographic Primitive Code Generation by Fiat

Mostly Automated Synthesis of Correct-by-Construction Programs

Building A Correct-By-Construction Proof Checkers For Type Theories

"Implementation and verification of catenable constant time deques"

Build dependency graphs between COQ objects

RISC-V Specification in Coq

An enhanced unification algorithm for Coq

Stdlib for the Rocq Prover

Relation algebra library for Coq