Hesper

A formally verifiable WebGPU / WGSL / PTX inference engine in Lean 4. Type-safe DSL, multi-backend (Vulkan / Metal / CUDA), production-grade Gemma 4 + BitNet runtimes.

Documentation

• Tutorial — chapter-by-chapter walk-through of the Shader DSL, verified ops + AD, multi-backend dispatch, BitNet + Gemma 4 end-to-end, and the Ch11 California Housing data-analysis case study.
• API reference — generated from source by doc-gen4. Covers every module reachable from Hesper.lean.

Benchmarks

• Hesper Kernel Micro-Benchmark
• BitNet b1.58 2B Inference (macOS Metal)

Source

github.com/Verilean/hesper