Lean lens implementation with custom notation.

Convert Lean .olean files to s-expressions

AQL Compiler to generate verilog code.

A project to map out the relations between different equational theories of Magmas.

A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

RISC-V emulator in python

A verification toolchain for Rust programs

Raylib bindings for Lean4

Concurrent decision diagram framework written in Rust

A (WIP) equality saturation tactic for Lean based on egg.

Lean 4 library of tools for parsing and compiling syntax and parser definitions.

Partial evaluator for Arm's Architecture Specification Language (ASL)

Mathlib search tool

Lean 4 programming language and theorem prover

General Application Store with support for root apps and more

Tactics for discharging Lean goals into SMT solvers.

Lean 4 port of Iris, a higher-order concurrent separation logic framework

Lean-formalizations of material from "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen

A quick reference for mapping Coq tactics to Lean tactics

A GitHub Action for suggesting Python type annotations.

Hydra is a framework for elegantly configuring complex applications

Isomorphism testing and automorphisms of graphs