Formal program design methods are most useful when sup ported with suitable mechanization. This need for mechanization has long been apparent, but there have been doubts whether verification technology could cope with the problems of scale and complexity. Though there is very little compelling evidence either way at this point, several powerful mechanical verification systems are now available for experimentation. Using SRI's PVS as one representative example, we argue that the technology of mechanical verification is already quite effective. PVS derives its power from an integration of theorem proving with type checking, decision procedures with interactive proof construction, and more recently, model checking with theorem proving. We discuss these individual aspects of PVS using examples, and motivate some of the challenges that lie ahead.

• mpc95.dvi
• mpc95.ps