The CompCert formally-verified C compiler

Cryptographic Primitive Code Generation by Fiat

Formal Reasoning About Programs

A framework for formally verifying distributed systems implementations in Coq

Verified Software Toolchain

Language for high-assurance and high-speed cryptography

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

Randomized Property-Based Testing Plugin for Coq