Hesper

Write GPU programs in Lean 4. Prove them correct. Run on WebGPU or CUDA.

[!IMPORTANT] Alpha software. APIs, verification features, and the compiler are under active development and subject to breaking changes. Current focus: BitNet, Gemma 4, and the verified-AD layer.

Hesper is a verified GPU programming framework. You write type-safe shaders and high-level tensor code in Lean 4, prove correctness with the same language, and run the result on WebGPU (Metal / Vulkan / D3D12) or CUDA PTX.

import Hesper.WGSL.DSL

-- Type-safe shader expressions, checked at Lean elaboration time:
let x : Exp (.scalar .f32) := var "x"
let y : Exp (.scalar .f32) := var "y"
let r := sqrt (x * x + y * y)              -- generates: sqrt(x*x + y*y)

-- let wrong := x + (var "i" : Exp (.scalar .i32))  -- ✗ type error

The Hesper Way

IP Catalog

See docs/CHANGELOG.md for the release timeline.

Quick Start

Option 1 — Tutorial Docker image (recommended)

A pre-built image with Lean 4, xeus-lean, Jupyter Lab, and all 12 tutorial chapters as runnable notebooks:

docker run --rm -p 8888:8888 ghcr.io/verilean/hesper-tutorial:latest
# → open http://localhost:8888 in your browser

Option 2 — Local build

git clone https://github.com/Verilean/hesper.git
cd hesper
lake build Hesper             # native deps (Dawn, Highway) build on demand
lake exe bitnet-complete      # first inference run

Prerequisites: Lean 4 (via elan), a C++17 toolchain, CMake ≥ 3.16. For Gemma 4 on CUDA: NVIDIA driver + CUDA Toolkit. Full setup instructions: docs/tutorial/md/Ch00_Setup.md.

Documentation

The tutorial is the canonical entry point. Each chapter is a Markdown master that's also rendered as a runnable Jupyter notebook via xeus-lean.

Other user-facing docs:

• docs/LORA_FINETUNING.md — BitNet LoRA training guide
• docs/VERIFIED_AD.md — Verified-AD design notes
• docs/circuit-dsl-tutorial.md — Kernel-fusion DSL deep-dive
• docs/research/ — Archived internal R&D notes (not maintained)

How It Works

┌──────────────────────────────────────────────────────────────┐
│  Lean 4 code                                                  │
│  ─ Type-safe shader DSL  ─ Tensor ops  ─ Formal proofs        │
└────────────────────────────┬──────────────────────────────────┘
                             ▼
┌──────────────────────────────────────────────────────────────┐
│  ShaderM IR  (a small imperative shader language in Lean)     │
└──────────────┬────────────────────────────┬───────────────────┘
               ▼                            ▼
┌─────────────────────────┐    ┌──────────────────────────────┐
│  WGSL backend           │    │  CUDA PTX backend             │
│  (Dawn native)          │    │  (libcuda driver API)         │
└──────────┬──────────────┘    └─────────────┬─────────────────┘
           ▼                                 ▼
   Metal / Vulkan / D3D12               NVIDIA GPU

The same DSL emits two surface languages. Pick the backend at compile time (-Kgpu=cuda for CUDA exes, default WebGPU otherwise).

Examples

lake exe bitnet-complete             # BitNet b1.58 inference end-to-end
lake exe gemma4-cuda data/...gguf "Hello"   # Gemma 4 on CUDA
lake exe tetris                      # Interactive WebGPU game
lake exe dsl-basics                  # Walk through the type-safe DSL
lake exe matmul-simple               # Smallest GPU matmul

The Examples/ directory has ~90 runnable demos organized by topic (DSL/, Compute/, Graphics/, MachineLearning/, …).

Project Structure

Hesper/
├── Hesper/             # Core library (DSL, WebGPU, CUDA, Layers, Models)
├── Examples/           # ~90 runnable demos
├── Tests/              # LSpec-based test suites
├── native/             # C++ FFI bridge (Dawn + CUDA driver shim)
├── c_src/              # Portable SIMD (Google Highway)
├── docs/
│   ├── tutorial/      # User-facing tutorial (Markdown master)
│   └── research/      # Internal R&D archive
└── lakefile.lean       # Lake build configuration

Testing

lake build test-all && ./.lake/build/bin/test-all

The same suite runs in CI across Linux + Vulkan, macOS + Metal, Windows + D3D12, and a CPU-only fallback path.

Contributing

See CONTRIBUTING.md. In short: fork, branch, run the test suite, open a PR. Bug reports and design discussions go to GitHub Issues / Discussions.

License

Apache-2.0. See LICENSE.

Acknowledgments

• Lean 4 — the language we're built on.
• Google Dawn — WebGPU native runtime.
• Google Highway — portable SIMD.
• Verilean / sparkle — sister project bringing the same verification ideas to hardware description.