The CompCert formally-verified C compiler

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

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

Formal Reasoning About Programs

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

My personal repository of formally verified mathematics.

Randomized Property-Based Testing Plugin for 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…

RISC-V Specification in Coq

Cuq: A MIR-to-Coq Framework Targeting PTX for Formal Semantics and Verified Translation of Rust GPU Kernels

Hoare Type Theory

A Lustre compiler in Coq

Coq library for verified low-level programming

LVC verified compiler

A Coq to Cedille compiler written in Coq

Bedrock Bit Vector Library

This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides bot…

Experiments in formalizing refinement type systems in Coq

All of the random projects, test files, helloworlds, proofs etc.

Coq formalization of a simple quantum imperative language, with Hoare-style logic.

Semi-automating verification of LLVM programs using Hoare Logic in Coq