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.

Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

Mathematical Components

Tricks you wish the Coq manual told you [maintainer=@tchajed]

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

Visual Studio Code extension for Coq

My personal repository of formally verified mathematics.

Mathematical Components compliant Analysis Library

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

A function definition package for Rocq

Verifying concurrent storage and distributed systems

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for embedded RISC-V systems with focus on a formally verified and auditable firmware.

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]

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

Goose converts a subset of Go to Rocq

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

A mechanisation of Wasm in Rocq

Monadic effects and equational reasoning in Rocq

A Rocq formalization of information theory and linear error-correcting codes

Documentation on goals of the Rocq-community organization, the shared contributing guide and code of conduct.

Rocq RFCs: documents to discuss changes to the Rocq Prover

Translate Python code to Rocq code for formal verification. Applied to the reference implementation of the Ethereum VM in Python (WIP, in pause)

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

Template project for program verification in the Rocq Prover, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]

Stdlib for the Rocq Prover

No description available

Mathematics of Robotic Manipulation using Rocq and MathComp

Rocqet proof language

Micromega tactics for Mathematical Components