The CompCert formally-verified C compiler

A Coq library for Homotopy Type Theory

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

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

Mostly Automated Synthesis of Correct-by-Construction Programs

A minimalistic blockchain consensus implemented and verified in Coq

Hoare Type Theory

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to…

Companion Coq development for Xavier Leroy's 2021 lectures on program logics

Program logic for developing and verifying distributed systems

Partial Commutative Monoids

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

A certified semantics for relational programming workout.

Intuitionistic Propositional Checker

Coq proof for "Games of Incomplete Information: a Framework Based on Belief Functions"

An mtl-like library for dealing with effects in Coq

Exercises for Coq course, based on SSReflect, Coq'Art and CPDT

Coherence of Heyting's first order arithmetic in Coq: "Proof assistants" project at LMFI, Paris-Diderot University (teacher: Pierre Letouzey)

Homotopy type theory