Despite the growing need to make software "bullet proof" against increasingly complex requirements and pervasive security attacks, testing can only go so far. Fortunately, formal program verification, which offers a practical complement to testing, and available technologies, like the SPARK toolset, can address specific requirements for robustness and functional correctness.