There is always loom for family.

Verified compiler from LambdaBox to WebAssembly, C, Rust, and OCaml

Lean playground for programming language modeling tooling.

Unified TUI and CLI to index and search your local coding agent session history across 11+ providers (Codex, Claude, Gemini, Cursor, Aider, etc.)

Display Zotero collection on E-Readers with KOReader

Verified HTTPS server in Lean 4 — TLS 1.3, HTTP/2, QUIC, WebSocket, gRPC — 914 machine-checked theorems, zero sorry. Pure library available (LeanServerPure).

FLOPS: Formalization in the Lean Theorem Prover of the P3109 Standard

An auto-active verifier embedded into Lean

SMT-based reasoning core for Lean4

Are We Fast Yet? Comparing Language Implementations with Objects, Closures, and Arrays

Yet another implementation of computer language benchmarks game

This work in progress aims to compare various HOT (higher-order and statically typed, a term coined by Phil Wadler) through reproducible course-grained, wall-time benchmarks. Our overall goals incl…

Electrum is a temporal extension to Alloy. Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in securi…

A model checker for relational first-order temporal specifications

The LTSmin model checking toolset

A deprecated equality saturation tactic for Lean based on egg.

SQLite bindings for Lean

TLA+ specifications and proofs of Logless Dynamic Reconfiguration in MongoDB Replication.

A certified RISC-V Interpreter with Hoare-logic in Lean

i18n library for Lean.

A modernised git interface for improved agent and human collaboration, review and control

A curated list of data oriented design resources.

Browser support for Lean using a monaco editor.

lean4 unit testing framework

A General-purpose Task-parallel Programming System in C++

Lean 4 theorem proving skill and workflow pack for AI coding agents

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.