An Iris-like proof mode for CompleteLattices

Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.

A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo

Separation Logic Proofs in Lean

A verifier for automated and interactive proofs about transition systems.

Mostly Automated Proof Repair for Verified Libraries

LeanSSR: an SSReflect-Like Tactic Language for Lean

Verified hash-based AMQ structures in Coq

A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2

Finite sets, finite maps, multisets and generic sets

Hahn: A Coq library

Formalization of the Truly Stateless Concurrency Model Checker in Coq

Mathematical Components

Generic model checker for concurrent C programs (mirror repository)

Verified Specifier of S-Graph Language

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

Archive for all Rocq and Coq-related opam packages organized in various repositories

Mechanized Theory of Event Structures

Coq library to deal with purely functional data structures