A Coq library for Homotopy Type Theory

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

Tricks you wish the Coq manual told you [maintainer=@tchajed]

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

Verified Software Toolchain

Language for high-assurance and high-speed cryptography

Verifying concurrent storage and distributed systems

Formalization of C++ for verification purposes.

Coq Lecture Notes (WIP)

Collection of Useful Features of the Coq Proof Assistant