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

A framework for formally verifying distributed systems implementations in Coq

Tricks you wish the Coq manual told you [maintainer=@tchajed]

Language for high-assurance and high-speed cryptography

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

Convert Haskell source code to Coq source code

FSCQ is a certified file system written and proven in Coq

Please see https://github.com/hacspec/hax

Lecture notes for a short course on proving/programming in Coq via SSReflect.

PeaCoq is a pretty Coq, isn't it?

A proof of false in Coq.

Formalising Type Theory in a modular way for translations between type theories

Dependent Object Types (DOT), bottom up

Formalization of the Dependent Object Types (DOT) calculus

LVC verified compiler

Writeup that goes along with this:

A formally verified compiler of untyped lambda calculus to brainfuck

System FR: Formalized Foundations for Stainless

Finite State Machines implemented in Coq.