A Coq library for Homotopy Type Theory

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

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

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

Modeling and Proving in Computational Type Theory

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Archived since the contents have been moved to the Hydras & Co. repository

Make your zero-knowledge circuits safe with formal verification! 🍀

Source code accompanying the Bachelor's thesis of Dominik Wehr.

Formalisation of my Master's Thesis in Coq.

Formalisation of Algebraic Geometry based on the HoTT library.