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.

An axiom-free formalization of category theory in Coq for personal study and practical work

Cryptographic Primitive Code Generation by Fiat

A framework for formally verifying distributed systems implementations in Coq

Convert Haskell source code to Coq source code

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

A Specification for Dependent Types in Haskell (Core)