The CompCert formally-verified C compiler

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

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.

Cryptographic Primitive Code Generation by Fiat

Formal Reasoning About Programs

Mathematical Components

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

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Verified Software Toolchain

A Learning Environment for Theorem Proving with the Coq proof assistant

Language for high-assurance and high-speed cryptography

Randomized Property-Based Testing Plugin for Coq

A Library for Representing Recursive and Impure Programs in Coq

A function definition package for Coq

Mathematical Components compliant Analysis Library

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

Verifying concurrent storage and distributed systems

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

Coq plugin embedding elpi

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

A library for formalizing Haskell types and functions in Coq

Mostly Automated Synthesis of Correct-by-Construction Programs

Coq formalizations of functional languages.

A library of mechanised undecidability proofs in the Coq proof assistant.

A framework for smart contract verification in Coq

Modeling and Proving in Computational Type Theory

A mechanisation of Wasm in Coq(Rocq)