A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

Cryptographic Primitive Code Generation by Fiat

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

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

Formal proof of the Four Color Theorem [maintainer=@ybertot]

A foundational framework for modular cryptographic proofs in Coq

Foundational Cryptography Framework for machine-checked proofs of cryptography.

A tiny toy formalization of Hoare logic for IMP with a proof of soundness