The CompCert formally-verified C compiler

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

A Coq library for Homotopy Type Theory

Formal verification tool for Rust: check 100% of execution cases of your programs to make safe applications for demanding domains.

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

Mathematical Components

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

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

Mathematical Components compliant Analysis Library

A formalization of geometry in Coq based on Tarski's axiom system

High level commands to declare a hierarchy based on packed classes

Replib: generic programming & Unbound: generic treatment of binders

A verified polyhedral scheduling validator in Coq.

HoTT proofs using experimental induction-induction (mostly about real numbers) (used to contain the HoTT.Classes proofs)

Library for structural temporal logic proofs over coinductive, free monads with effects and choice.