Kuiper is a language for safe and verified GPU program- ming based on dependent types and concurrent separation logic. Kuiper models the intricacies of the GPU programming model, including the memory hierarchy, kernel launches, and synchronization within a single comprehensive framework. Memory bugs and data races are ruled out for any well-typed program. Optionally, full functional-correctness proofs can be performed. Kuiper programs can be heavily polymorphic (over types, operations, memory layout, and more) and ex- tract to efficient, specialized CUDA code. We use Kuiper to implement several common GPU kernels (matrix multi- plication, reductions, softmax). Kuiper is built over the F★ [Swamy et al. 2016] ecosystem.