Project Titania is a complete large language model system, from transformer to transistor, simple enough for one person to understand.

wzv — record now, get waveforms later

Fast Opportunistic Mixture-Of-Experts. From-scratch C/HIP MoE inference with multi-tier caching and cache-aware routing. First ever example of running Qwen3.5-397B at 5–9 tok/s on a $2,100 desktop.

TorchLean is the first unified Lean 4 framework for neural-network specification, execution, and verification.

Self-hosted AI workspace.

A standalone, FP4-quantized General Matrix Multiply (GEMM) core, from RTL through synthesis and full place-and-route in the OpenLane 2 flow on the SkyWater SKY130 process.

# AXI SVA Assertion Library SystemVerilog assertion library for AXI4 and AXI4-Lite, derived from *ARM IHI 0022C — AMBA AXI Protocol Specification v2.0*.

Wolfram Language / Mathematica reimplementation in Rust (Wolfram oxidized)

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.

A collection of formalized statements of conjectures in Lean.

VHDL compiler and simulator

VHDL compiler and simulator

A core language for rule-based hardware design 🦑

Mirage Persistent Kernel: Compiling LLMs into a MegaKernel

An open-source, GPU-accelerated physics simulation engine built upon NVIDIA Warp, specifically targeting roboticists and simulation researchers.

Datatypes as quotients of polynomial functors

A WIP definitional (co)datatype package for Lean4

Reinforcement learning in differentiable multiphysics simulation with NVIDIA Warp.

FlashMLA: Efficient Multi-head Latent Attention Kernels

A Python implementation of the Herbert game from the Imagine Cup algorithm contest.

Pre-built components and code samples to help you build and deploy production-grade AI applications with the OpenVINO™ Toolkit from Intel

Moshi is a speech-text foundation model and full-duplex spoken dialogue framework. It uses Mimi, a state-of-the-art streaming neural audio codec.

A high-performance, zero-overhead, extensible Python compiler with built-in NumPy support

Neural Optimal Transport with Lagrangian Costs

Official implementation of our paper "Scalable Event-by-event Processing of Neuromorphic Sensory Signals With Deep State-Space Models"

Training efficient drone controllers with Analytic Policy Gradient