Docker images of the Rocq Prover (see also: https://github.com/rocq-community/docker-coq-action) [maintainer=@Justme0606]

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 environmen…

Multi platform setup for Coq, Coq libraries and tools

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

A generic goal preprocessing tool for proof automation tactics in Coq

Theory and Lindemann theorem

A gently curated list of companies using verification formal methods in industry

Computing Pi decimal using Plouffe Formula in Coq