Cosette is an automated SQL solver.

Demo for high-performance type theory elaboration

Bug-free machine learning on stochastic computation graphs

Lean 4 kernel / 'external checker' written in Lean 4

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.

Write C shims from within Lean code.

A quick reference for mapping Coq tactics to Lean tactics

Separation Logic Proofs in Lean

An experimental mutual induction tactic for Lean 4.

A Lean implementation of Interaction Trees

Lean playground for programming language modeling tooling.

Formalizing the stable marriage problem and the Gale-Shapley algorithm in Lean

Mini crush tactic example