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.

Total Parser Combinators in Coq [maintainer=@womeier]

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