A library for building dynamic webapps, using Js_of_ocaml

Zerocopy makes zero-cost memory manipulation effortless. We write `unsafe` so you don’t have to.

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

/r/Showerthoughts fortune file generator

Verified Rust for low-level systems code

High-precision, one-shot and consistent benchmarking framework/harness for Rust. All Valgrind tools at your fingertips.

A capability-based microkernel written in Lean 4

An seL4 reference webserver application

LLM-assisted Lean specification of neural architectures with IREE codegen.

A search engine for Lean 4 declarations

Official codebase for I-JEPA, the Image-based Joint-Embedding Predictive Architecture. First outlined in the CVPR paper, "Self-supervised learning from images with a joint-embedding predictive arch…

[NeurIPS 2025 Spotlight] TPA: Tensor ProducT ATTenTion Transformer (T6) (https://arxiv.org/abs/2501.06425)

NanoGPT (124M) in 90 seconds

A minimal development of SSA theory

Definitional implementation of Cedar language and utilities for DRT

The best ChatGPT that $100 can buy.

Original Apollo 11 Guidance Computer (AGC) source code for the command and lunar modules.

HPC Rust LLM Tokenizer Suite

A Proof-oriented Programming Language

This is a program that uses the Contributions tracker as a marquee display.

Gemma open-weight LLM library, from Google DeepMind

♞ lichess.org: the forever free, adless and open source chess server ♞

LEAN4 AUTO YOUTUBE LIVING

Train the smallest LM you can that fits in 16MB. Best model wins!

Lean 4 Zstandard (RFC 8878) decompression: C FFI bindings and pure-Lean implementation with formal proofs

Ground Zero: Lean 4 HoTT Library