A Coq library for Homotopy Type Theory

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Cryptographic Primitive Code Generation by Fiat

A framework for formally verifying distributed systems implementations in Coq

Mathematical Components

Verified Software Toolchain

A Library for Representing Recursive and Impure Programs in Coq

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

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Collapsing Towers of Interpreters

A compiler plug-in to control object lifetimes in Scala

Program logic for developing and verifying distributed systems

working with coq and tezos

A certified semantics for relational programming workout.

State-Transition Systems for Smart Contracts

An itree-like data-structure to additionally support internal non-determinism

Pi-calculus in Coq

System FR: Formalized Foundations for Stainless

BDD based symbolic model checker for the modal mu-calculus

Special uses

Short, fun proofs in Coq