Weightproof verifies LLM inference on Rust, CUDA, Lean

The author introduces Weightproof, an experimental proof stack designed to verify exact dense integer-model execution for LLM inference using Rust, CUDA, and Lean. The implementation checks complete execution statements against committed model weights and residual traces, avoiding general zkVMs in favor of bespoke multilinear proofs and formal GPU kernel verification. While it currently operates on smaller fixtures rather than full 8B checkpoints, the system demonstrates practical verification performance and byte-identical outputs across CPU and GPU backends. Open article →