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.

Mathematical Components

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

A function definition package for Coq

Mathematical Components compliant Analysis Library

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

Coq plugin embedding elpi

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

RISC-V Specification in Coq

High level commands to declare a hierarchy based on packed classes

Coq development for the course "Mechanized semantics", Collège de France, 2019-2020

Stdlib for the Rocq Prover

Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020

Compositional Verification of Composite Byzantine Protocols

who needs type constructor? (in lean 4)