The CompCert formally-verified C compiler

A Coq library for Homotopy Type Theory

This coq 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

Cryptographic Primitive Code Generation by Fiat

Formal Reasoning About Programs

Mathematical Components

A framework for formally verifying distributed systems implementations in Coq

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

Sail RISC-V model

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

Verified Software Toolchain

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

A Learning Environment for Theorem Proving with the Coq proof assistant

A work-in-progress language and compiler for verified low-level programming

My personal repository of formally verified mathematics.

Language for high-assurance and high-speed cryptography

Randomized Property-Based Testing Plugin for Coq

A function definition package for Coq

Mathematical Components compliant Analysis Library

A Library for Representing Recursive and Impure Programs in Coq

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older versio…

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

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

🐣 A blog engine written and proven in Coq

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

Proofs in Coq for the book Reflective Programs in Tree Calculus

Mostly Automated Synthesis of Correct-by-Construction Programs

A core language for rule-based hardware design 🦑