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.

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

An axiom-free formalization of category theory in Coq for personal study and practical work

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

A function definition package for Coq

Mathematical Components compliant Analysis Library

Verifying concurrent storage and distributed systems

Lecture notes for a short course on proving/programming in Coq via SSReflect.

Formal specification and verification of hardware, especially for security and privacy.

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

High level commands to declare a hierarchy based on packed classes

Coq in a Hurry - Exercises