Cryptographic Primitive Code Generation by Fiat

Formal Reasoning About Programs

Mathematical Components

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

Randomized Property-Based Testing Plugin for Coq

Convert Haskell source code to Coq source code

A function definition package for Rocq

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

Public snapshots of "ACSL by Example"

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

A library for effects in Coq.

Distributed Data Structures in Coq