We introduce Kuiper, a language for safe and verified efficient CPU/GPU programming embedded as an
extensible library within the F* dependently typed language. We rely on F*’s support for dependent types and its
associated Pulse concurrent separation logic to develop a program logic in which to prove CPU/GPU programs
safe, data-race free, and functionally correct. Our model of the GPU includes several intricacies, including the
memory hierarchy, kernel launches, and synchronization within a single comprehensive framework. To do so,
we extend the Pulse program logic with a novel notion of located resources and a new connective to structure
reasoning about massively parallel programs, and present new proof rules to lift the per-thread view of GPU
kernels to an end-to-end correctness specification.

We have used Kuiper to program and prove correct a variety of GPU kernels, including full functional
correctness proofs of an optimized matrix multiplication using two levels of block tiling and tensor cores. In
doing so, we have developed a range of libraries to enable programs and proofs at a high level of abstraction
but without imposing any runtime overhead. These allow Kuiper programs to be polymorphic (over types,
operations, memory layout, and more) and compile to efficient, specialized CUDA code, while enabling a
novel form of verified auto-tuning. Our experimental evaluation confirms that Kuiper programs match the
performance of their handwritten CUDA counterparts and are competitive with closed source, state-of-the-art
kernels in cuBLAS.