rocq

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

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

Visual Studio Code extension for Rocq

My personal repository of formally verified mathematics.

Formal verification for OCaml, with Rocq

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

Mathematical Components compliant Analysis Library

Verifying concurrent storage and distributed systems

A function definition package for Rocq

A curated list of awesome Coq frameworks, libraries and software.

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]

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

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