Main public package repository for OPAM, the source package manager of OCaml.

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx]

High level commands to declare a hierarchy based on packed classes

Ring, field, lra, nra, and psatz tactics for Mathematical Components

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…

A generic goal preprocessing tool for proof automation tactics in Coq

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Coq plugin embedding elpi

Mathematical Components compliant Analysis Library

Mathematical Components

The formal proof of the Odd Order Theorem

Language for high-assurance and high-speed cryptography

A framework for formally verifying distributed systems implementations in Coq

Archive for all Rocq and Coq-related opam packages organized in various repositories

Verifying concurrent crash-safe systems

Formalization of C++ for verification purposes.

The code for my Master Thesis

Nix Packages collection

Pygments is a generic syntax highlighter written in Python

Partial Commutative Monoids

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

Coq Enhancement Proposals

A composable build system for OCaml.

A plugin for Coq to add dependent pattern-matching.

Visual Studio Code Extension and Language Server Protocol for Coq