The CompCert formally-verified C compiler

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

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

Formal Reasoning About Programs

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

A core language for rule-based hardware design 🦑

Modeling and Proving in Computational Type Theory

The mathematical study of type theories, in univalent foundations

RISC-V Specification in Coq

Formalization of Machine Learning Theory with Applications to Program Synthesis

Companion Coq development for Xavier Leroy's 2021 lectures on program logics

Problem Sets for MIT 6.512 Formal Reasoning About Programs, Spring 2023

A Coq formalization of the textbook Categories and Toposes: Visualized and Explained

Programs and Proofs -- Spring 2025 -- IITM

Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2020

QuickChick demo for CIS 700