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.

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

Verified Software Toolchain

A work-in-progress language and compiler for verified low-level programming

A Library for Representing Recursive and Impure Programs in Coq

Coq plugin embedding elpi

A Verified Compiler for Gallina, Written in Gallina

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

Formal specification and verification of hardware, especially for security and privacy.

Public snapshots of "ACSL by Example"

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

A foundational framework for modular cryptographic proofs in Coq

Bounds on divsteps iterations in safegcd

A Coq library for parametric coinduction