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

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

A verification toolchain for Rust programs

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq

Visual Studio Code extension for Coq

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

A Seamless, Interactive Tactic Learner and Prover for Coq

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

A Coq Mechanization of ECMAScript 2023 Regexes

A verified(?) TCP client/server chat application

OCaml module of Nijn to generate coq scripts for checking termination proofs of higher-order rewriting systems.

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 development of machine-checked proofs.

A simple first order logic theorem prover using tableaux

Dead-Simple Build System for Coq

Formal verification for OCaml

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Library of useful utility functions for Coq plugins

Pure Demand Operational Semantics

Prettify the output of coq makefiles

Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]