The CompCert formally-verified C compiler

A Coq library for Homotopy Type Theory

Formal Reasoning About Programs

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

Convert Haskell source code to Coq source code

Randomized Property-Based Testing Plugin for Coq

A formalization of geometry in Coq based on Tarski's axiom system

A minimalistic blockchain consensus implemented and verified in Coq

Lecture material for DeepSpec Summer School 2017

A library for effects in Coq.

GoNative project: formal machines models in Coq

Control-flow based language verification framework