DiffDog: Formally Verified Automatic Differentiation at Billion-Parameter Scale

As AI training runs grow in scale, cost, and complexity, software errors become increasingly consequential. Yet mainstream automatic differentiation (AD) libraries at the heart of these training runs rely on Python-centered stacks that are unable to provide machine-checkable correctness guarantees. We present \DiffDog, a formally verified AD system in Lean that supports arbitrarily nested forward- and reverse-mode AD, automatic vectorization, and compilation to GPU and TPU executables, with machine-checked correctness proofs for its tracing, differentiation, and vectorization transformations. Programs written against \DiffDog's abstract array interface can be instantiated over mathematical value types for direct reasoning and over traceable array types for compilation to accelerators. This dual interpretation provides an extensible foundation for developing verified models, numerical algorithms, and program transformations without relinquishing high-performance accelerated execution. We exhibit \DiffDog's expressiveness and utility by training a language model with verified gradients, introducing the first accelerator-executable SGD optimizer with verified $O(1/\sqrt{T})$ convergence, and demonstrating that \DiffDog automatically synthesizes a counterexample to Adam's original convergence claim, independently exposing the failure identified by DBLP:conf/iclr/ReddiKK18. Finally, \DiffDog's training and inference throughput is competitive with optimized JAX and PyTorch implementations on leading open-weight models, including Qwen 3.8-27B and Gemma 4.