A Coq library for Homotopy Type Theory

An axiom-free formalization of category theory in Coq for personal study and practical work

Cryptographic Primitive Code Generation by Fiat

Formal Reasoning About Programs

Language for high-assurance and high-speed cryptography

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

Voevodsky's original development of the univalent foundations of mathematics in Coq

A Library for Representing Recursive and Impure Programs in Coq

Mathematical Components compliant Analysis Library

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

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

🐣 A blog engine written and proven in Coq

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

A library for formalizing Haskell types and functions in Coq

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

Coq formalizations of functional languages.

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

A library of mechanised undecidability proofs in the Coq proof assistant.

Verified hash-based AMQ structures in Coq

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

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

Collapsing Towers of Interpreters

Lecture material for DeepSpec Summer School 2017

Dependent Object Types (DOT), bottom up

Hoare Type Theory

Formalization of Machine Learning Theory with Applications to Program Synthesis

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]