Will Sturgeon

Algolean. Algorithms and Complexity Library using the lightweight query combinator framework called "Prog"

num-bigint. Big integer types for Rust

lean64. doom64 but lean

json. Strongly typed JSON library for Rust

toric. Formalisation of toric varieties in Lean 4

afl-rs-logo. Rust

redqueen. Python

nix-doom-emacs-unstraightened. Builds Doom Emacs using Nix

vcaml. OCaml bindings for the Neovim API

halflife. Half-Life 1 engine based games

disp. Aspiring universal programming language. Features: user-definable syntax and types + self-improving optimizer that creates provably correct, hardware-optimal programs from formal specification. Bootstrapped on Barry Jay's reflective tree calculus.

mlton. The MLton repository

mirage. MirageOS is a library operating system that constructs unikernels

import-tree. Import all nix files in a directory tree.

core. An Emacs framework for the stubborn martian hacker

C-parsing-for-Lean4. A parser for ANSI C, in Lean4.

llvm-profparser. Mostly complete pure rust implementation of parsing llvm instrumentation profile data

fhm. A Hindley-Milner language formalised in Lean 4 – proven type-safe, and runnable

ProofWidgets4. Helper toolkit for creating your own Lean 4 UserWidgets

miri. An interpreter for Rust's mid-level intermediate representation

TauCeti. An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

cargo-llvm-cov. Cargo subcommand to easily use LLVM source-based code coverage (-C instrument-coverage).

nanobruijn. Experimental Lean 4 type checker using pure de Bruijn indices

evm_proof_checker. Lean proof kernel in solidity

lean4-nix. Nix overlay for Lean 4, and lake2nix

LeanArchitect. LeanArchitect extracts a blueprint directly from Lean source.

isa_top_autoform1. Isabelle

verso. Lean documentation authoring tool

Erdos90. Formal Lean proof of OpenAI's 2026 counterexample to the Erdős unit distance conjecture

beamer. A LaTeX class for producing presentations and slides

sisyphus. Mostly Automated Proof Repair for Verified Libraries

malfunction. Malfunctional Programming

rocq-verified-extraction. Verified Extraction from Rocq to OCaml/Malfunction

lean4-bdd. Binary Decision Diagrams in Lean 4

jacobian-claude. Claude code trying to formalize Jacobians. I don't understand the math, and haven't reviewed any of this.

cakeml. CakeML: A Verified Implementation of ML

flux. Refinement Types for Rust

liquid-fixpoint. Horn Clause Constraint Solving for Liquid Types

evcxr. Rust

paco. A Coq library for parametric coinduction

hazel. Hazel, a live functional programming environment with typed holes

loom. Concurrency permutation testing tool for Rust.

flowistry. Flowistry is an IDE plugin for Rust that helps you focus on relevant code.

super-productivity. Super Productivity is an advanced todo list app with integrated Timeboxing and time tracking capabilities. It also comes with integrations for Jira, GitLab, GitHub and Open Project.

taskwarrior. Taskwarrior - Command line Task Management

bonsai. A library for building dynamic webapps, using Js_of_ocaml

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

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

showerthoughts. /r/Showerthoughts fortune file generator

verus. Verified Rust for low-level systems code

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

llm-jepa. Python

SplineSans. Python

seLe4n. A capability-based microkernel written in Lean 4

sel4webserver. An seL4 reference webserver application

lean4-mlir. Lean specification of neural architectures with verified IREE codegen.

lean-explore. A search engine for Lean 4 declarations

ijepa. 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 architecture."

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

modded-nanogpt. NanoGPT (124M) in 90 seconds

lean-mlir. A minimal development of SSA theory

cedar-spec. Definitional implementation of Cedar language and utilities for DRT

nanochat. The best ChatGPT that $100 can buy.

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

wordchipper. HPC Rust LLM Tokenizer Suite

FStar. A Proof-oriented Programming Language

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

gemma. Gemma open-weight LLM library, from Google DeepMind

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

automath. LEAN4 AUTO YOUTUBE LIVING

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

gkylcas. Common Lisp

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

lean-zip. Lean

ground_zero. Ground Zero: Lean 4 HoTT Library

HoTTLean. Lean

UniMath. This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

TypeTheory. The mathematical study of type theories, in univalent foundations

initiality. A formalized proof of a version of the initiality conjecture

sflean.github.io.

mimalloc. mimalloc is a compact general purpose allocator with excellent performance.

comparator. Lean

zkLean. zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements

cslib. The Lean Computer Science Library (CSLib)

lean-kernel-arena. Lean

loogle. Mathlib search tool

opencode. The open source coding agent.

aeneas. A verification toolchain for Rust programs

harmonia. Nix binary cache implemented in rust (maintainer: @Mic92)

home-manager. Manage a user environment using Nix [maintainer=@khaneliman, @rycee]

btop. A monitor of resources

lean4export. Plain-text declaration export for Lean 4

infrastructure. The Noisebridge Infrastucture

spotatui. A fast, standalone terminal music player in Rust: native Spotify streaming plus local, Subsonic, radio, and YouTube sources.

shell. A fluid, morphing shell for your Linux desktop

QuickChick. Randomized Property-Based Testing Plugin for Coq

type-system-chess. Chess implemented entirely in the Rust and TS type systems.

nbradio. nbradio served from beyla.local @ Noisebridge

cosmic-epoch. Next generation Cosmic desktop environment

avahi. Avahi - Service Discovery for Linux using mDNS/DNS-SD -- compatible with Bonjour

par-lang. Par (⅋) is an experimental concurrent programming language. It's an attempt to bring the expressive power of linear logic into practice.

coreutils. Cross-platform Rust rewrite of the GNU coreutils

surge. Synthesizer plug-in (previously released as Vember Audio Surge)

gearmulator. Low Level Emulation of classic VA synths & effects of the late 90s/2000s by emulating the used ICs

plzoo. Programming Languages Zoo

aHash. aHash is a non-cryptographic hashing algorithm that uses the AES hardware instruction

dashmap. Blazing fast concurrent HashMap for Rust.

conc-map-bench. Rust

hashbrown. Rust port of Google's SwissTable hash map

l4v. seL4 specification and proofs

seL4. The seL4 microkernel

motor-os. A simple, fast, and secure operating system for the cloud.

algorithmica. A computer science textbook

kani. Kani Rust Verifier

alioth. Experimental Type-2 hypervisor, written from scratch in Rust, runs on Linux and macOS.

microvm.nix. NixOS MicroVMs

quibbler. Python

hott-notes. 15-819 (Homotopy Type Theory) Lecture Notes

book. A textbook on informal homotopy type theory

sHoTT. Formalisations for simplicial HoTT and synthetic ∞-categories.

infinity-cosmos. A blueprint for a formalization of infinity-cosmos theory in Lean.

oxcaml. OCaml - Oxidized!

strongpnt. Lean

rocq-lsp. Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]

LeanMillenniumPrizeProblems. Formalization of the Millennium Problems in Lean 4

verina. Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.

mathlib4. The math library of Lean 4

tmux. tmux source code

erdosproblems. A community database for the problems on the erdosproblems.com site

kwin-effects-forceblur. Fork of the Plasma 6 blur effect with additional features (including force blur) and bug fixes.

BLAKE3. the official Rust and C implementations of the BLAKE3 cryptographic hash function

stm. Software Transactional Memory

triton. Development repository for the Triton language and compiler

rust_transformer. A transformer built from scratch in Rust.

LeanHammer. LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.

lean-premise-server. Premise selection server for Lean

LeanStateSearch. TypeScript

pragmatapro. PragmataPro font is designed to help pros to work better

inter. The Inter font family

LeanInteract. LeanInteract: A Python Interface for Lean 4

VST. Verified Software Toolchain

nanoda_lib. Library implementing type inference/checking functionality based on the Lean theorem prover

mm0. Metamath Zero specification language

Iosevka. Versatile typeface for code, from code.

LeanSearch. Python

leanblueprint. plasTeX plugin to build formalization blueprints.

ngt-rs. Rust wrappers for NGT approximate nearest neighbor search

gpt-oss. gpt-oss-120b and gpt-oss-20b are two open-weight language models by OpenAI

metamath-knife. Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.

lean4. Lean 4 programming language and theorem prover

lean.nvim. Neovim support for the Lean theorem prover

FLT. Ongoing Lean formalisation of the proof of Fermat's Last Theorem

zen-browser-flake. Community-driven Nix Flake for the Zen browser

desktop. Welcome to a calmer internet

Forecasting_Bot_Q2. Python

certirocq. A Verified Compiler for Gallina, Written in Gallina

CompCert. The CompCert formally-verified C compiler

cubical. An experimental library for Cubical Agda

Coq-HoTT. A Coq library for Homotopy Type Theory

cubicaltt. Experimental implementation of Cubical Type Theory

Mailspring. :love_letter: A beautiful, fast and fully open source mail client for Mac, Windows and Linux.

rust-raspberrypi-OS-tutorials. :books: Learn to write an embedded OS in Rust :crab:

rustls-embedded-demo. Demo for embedded use of rustls

mujoco. Multi-Joint dynamics with Contact. A general purpose physics simulator.

asusctl. Daemon and tools to control your ASUS ROG laptop. Supersedes rog-core.

linux-nixos-hyprland-config-dotfiles. Linux 🐧 configuration based on NixOS ❄️, Hyprland, and Catppuccin Macchiato theme 😸 for a consistent, complete, and customizable experience. 🚀

Hyprland. Hyprland is an independent, highly customizable, dynamic tiling Wayland compositor that doesn't sacrifice on its looks.

dots-hyprland. Usability-first dotfiles

picoserve. An async no_std HTTP server suitable for bare-metal environments, heavily inspired by axum

esp32-camera. C

wezterm. A GPU-accelerated cross-platform terminal emulator and multiplexer written by @wez and implemented in Rust

coqhammer. CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory

mup. maximal update parametrization (µP)

BernNet. PyTorch implementation of "BernNet: Learning Arbitrary Graph Spectral Filters via Bernstein Approximation"

jax_dataclasses. Pytrees + dataclasses ❤️

flaxformer. Python

cerberus. Cerberus C semantics

rss2email. Forward RSS feeds to your email address, community maintained

jax. Composable transformations of Python+NumPy programs: differentiate, vectorize, JIT to GPU/TPU, and more

ARENA_3.0. Jupyter Notebook

blog_os. Writing an OS in Rust

spotify-tui. Spotify for the terminal written in Rust 🚀

git. Git Source Code Mirror - This is a publish-only repository but pull requests can be turned into patches to the mailing list via GitGitGadget (https://gitgitgadget.github.io/). Please follow Documentation/SubmittingPatches procedure for any of your improvements.

ayu. 🎨🖌 Modern, bright color theme for Sublime Text

nix-darwin. Manage your macOS using Nix

ayu-vim. Modern theme for modern VIMs

vim. The official Vim repository

rocq. The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

direnv. unclutter your .profile

helix. A post-modern modal text editor.

logseq. A privacy-first, open-source platform for knowledge management and collaboration. Download link: http://github.com/logseq/logseq/releases. roadmap: https://logseq.io/p/NX4mc_ggEV

kitty. If you live in the terminal, kitty is made for you! Cross-platform, fast, feature-rich, GPU based.

nix. Nix, the purely functional package manager

xla. A machine learning compiler for GPUs, CPUs, and ML accelerators

embassy. Modern embedded framework, using Rust and async.

rust. Empowering everyone to build reliable and efficient software.

linux. Linux kernel source tree

atsamd. Target atsamd microcontrollers using Rust