Message Passing Interface (MPI) is widely considered to be the lingua-franca of High Performance Computing (HPC). Indeed, it is a fact that most supercomputers in recent times run programs developed using MPI. Nevertheless, developing MPI programs that are correct and performant remains a huge challenge. In this talk, I will first discuss some of the strategies that we developed to formally verify MPI programs for correctness (such as absence of communication deadlocks, violations of safety assertions, etc.). I will then discuss how we can build automated performance tuners for MPI applications using the discussed verification techniques.