Separation Logic Proofs in Lean

A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit your PRs here.

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 Coq related OPAM packages organized in various repositories

Mechanized Theory of Event Structures

Coq library to deal with purely functional data structures