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

FSCQ is a certified file system written and proven in Coq

A function definition package for Rocq

Coq formalizations of functional languages.

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

A web server written in Coq.

A library for effects in Coq.

Distributed Data Structures in Coq