Abstract
In this talk I will introduce the aim of program verification and I will discuss the challenges and benefits of its use in support of differential privacy. I will discuss some of the steps taken so far in this direction, and some of the main challenges for future applications.