The CompCert formally-verified C compiler

A Coq library for Homotopy Type Theory

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

Formal Reasoning About Programs

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

Verified Software Toolchain

Randomized Property-Based Testing Plugin for Coq

Voevodsky's original development of the univalent foundations of mathematics in Coq

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

Coq plugin embedding elpi

A Verified Compiler for Gallina, Written in Gallina

A minimalistic blockchain consensus implemented and verified in Coq

High level commands to declare a hierarchy based on packed classes

xmonad in Coq

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

Library for Classical Coq

Formalization of the polymorphic lambda calculus and its parametricity theorem

Partial Commutative Monoids

A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems

Intermediate Memory Model (IMM) and compilation correctness proofs for it

Hahn: A Coq library

A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq

Semantics for Cryptol

Verified Extraction from Rocq to OCaml/Malfunction

Coq plugin for extracting Rust code

Reflective verification procedures for separation logic programs in Coq