Mathematical Components

Visual Studio Code extension for Rocq

My personal repository of formally verified mathematics.

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

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

A Verified Compiler for Gallina, Written in Gallina

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

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

Rocq RFCs: documents to discuss changes to the Rocq Prover

Formal verification for Solidity smart contracts with the theorem prover Rocq. Providing higher security in a time of smarter AIs.

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]

Micromega tactics for Mathematical Components

Stable sort algorithms and their stability proofs in Rocq

Agentic Theorem Prover for Rocq for Program Verification

OCaml as a Tactic Language for the Rocq Prover

Translation of HOL-Light's Multivariate library in Rocq

HOL-Light to Dedukti/Lambdapi translator

Syntax extensions for quoting Rocq terms in OCaml