veil Public

A verifier for automated and interactive proofs about transition systems.

verse-lab/veil's past year of commit activity

Lentil Public

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

verse-lab/Lentil's past year of commit activity

weird-logic Public

Hyper-safety reasoning for provably realisable program exploits.

irl Public

Infinitary Relation Logic

verse-lab/irl's past year of commit activity

loom Public

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.

verse-lab/loom's past year of commit activity

loom2 Public

There is always loom for family.

verse-lab/loom2's past year of commit activity

velvet Public

An auto-active verifier embedded into Lean

verse-lab/velvet's past year of commit activity

ego Public

EGraphs in OCaml

verse-lab/ego's past year of commit activity

yolo Public

Lazy Proof Automation for Separation Logic

verse-lab/yolo's past year of commit activity