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

Verifying concurrent storage and distributed systems

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

Mathematical Components compliant Analysis Library

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]

Theorem statements about OSS-Fuzz fuzz targets as compiled RISC-V binaries, and machine-checked Rocq proofs of them

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

OSS Verify: enrollment and build instructions for formally verifying open-source fuzz targets

Rocq formalisation of the lambda calculus with partial substitutions

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

A Rocq model of a Linux process that runs a RISC-V binary