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! ✈️ 🚀 ⚕️ 🏦

Formal Reasoning About Programs

Mathematical Components

Verified Software Toolchain

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

Modeling and Proving in Computational Type Theory

Formalization of C++ for verification purposes.

Formalization of the Truly Stateless Concurrency Model Checker in Coq

An implementation of lambda weak omega in Coq, with report.

The well-foundedness of the multiset ordering

Verification of GoJournal