The CompCert formally-verified C compiler

A Coq library for Homotopy Type Theory

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

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

Formal Reasoning About Programs

Mathematical Components

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

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

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older versio…

🐣 A blog engine written and proven in Coq

Verified hash-based AMQ structures in Coq

The mathematical study of type theories, in univalent foundations

RISC-V Specification in Coq

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

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

A framework for implementing and certifying impure computations in Coq

A blog about Coq

Total Parser Combinators in Coq [maintainer=@womeier]

A Certified Interpreter for ML with Structural Polymorphism

Repository where I'll collect some demos of proof assistants that I show to various people in order to spread the magic

Ring, field, lra, nra, and psatz tactics for Mathematical Components

Formalization of the polymorphic lambda calculus and its parametricity theorem

Brainfuck formalized in Coq

Resources for "One Monad to Prove Them All"

Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]

An encoding of linear logic in Coq with minimal Sokoban and blocks world examples

Calculus of Constructions

Theorems for Real Closed Fields