A framework for formally verifying distributed systems implementations in Coq

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

A framework for smart contract verification in Coq

A Small Quantum Intermediate Representation

This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance …

Programs and Proofs -- Spring 2025 -- IITM

Library for structural temporal logic proofs over coinductive, free monads with effects and choice.