Verified Systems Engineering Lab

A verifier for automated and interactive proofs about transition systems.

(at least a useful portion of) Temporal Logic of Actions, a.k.a. TLA in Lean 4

Hyper-safety reasoning for provably realisable program exploits.

Infinitary Relation Logic

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.

There is always loom for family.

An auto-active verifier embedded into Lean

EGraphs in OCaml

Lazy Proof Automation for Separation Logic