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

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

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

Verifying concurrent storage and distributed systems

A minimalistic blockchain consensus implemented and verified in Coq

Formalization of C++ for verification purposes.

Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).

Coq Lecture Notes (WIP)

Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]

Tiny verified SAT-solver

BGP Policy Verification

Formal Semantics for Why3

Coq BPF interpreter

Formalization of the Truly Stateless Concurrency Model Checker in Coq

Initial tinkering with a BPF metalanguage and implementation formally verified in Coq.

Formal Verification of an Incremental Garbage Collector

Assignment repo for Systems Verification Fall 2024 at UW-Madison

Universal Ctags optlib parser for Coq

Coq library to deal with purely functional data structures

Correctness of RSA algorithm