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.

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

Coq Lecture Notes (WIP)

Proving crash safety for systems with layered recovery

Collection of Useful Features of the Coq Proof Assistant