A verifier for automated and interactive proofs about transition systems.

Tactics for discharging Lean goals into SMT solvers.

This project demonstrates a grammar repair framework.

An auto-active verifier embedded into Lean

LeanSSR: an SSReflect-Like Tactic Language for Lean

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 template repository with an example of using Veil verifier as a Lean library.

Separation Logic Proofs in Lean

Lean web editor

Helper toolkit for creating your own Lean 4 UserWidgets