Mathematical Components

Visual Studio Code extension for Coq

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]

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

A Verified Compiler for Gallina, Written in Gallina

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. Ensure no vulnerabilities for your smart contracts.

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

HOL-Light to Dedukti/Lambdapi translator

Translation of HOL-Light's Multivariate library in Rocq

Exploring formal computation, lambda calculus, and program verification with ROCQ (Coq).

Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat