The development of GPU software requires techniques that support developers to produce software that is both functionally correct and high-performing. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow.