A Coq library for Homotopy Type Theory

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

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

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

Mathematical Components

Metaprogramming, verified meta-theory and implementation of Coq in Coq

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

Mathematical Components compliant Analysis Library

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

Modeling and Proving in Computational Type Theory

Gallina to Bedrock2 compilation toolkit

A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]

Prime numbers for Coq

Denotational Semantics of the Untyped Lambda Calculus

The TacTok automated Coq proof script synthesis tool

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