This talk shows how to use the specification and verification system PVS as a framework for formal software development. Software is developed according to the methodology of stepwise refinement: starting from an abstract requirement specification a series of correctness-preserving development steps is applied to obtain an executable and efficient program. We use PVS to provide a fully mechanized treatment of the transformational development process which comprises the formalization (i.e., implementation in the PVS specification language), verification, and correct application of development steps and development methods. A rigorous formal treatment is important since it greatly increases the confidence in the soundness of transformations and their application to specific problems. The software development steps presented in this talk include the well-known algorithmic paradigm of divide-and-conquer, the optimization transformation finite differencing, and an example of data structure refinement (implementing finite sets by binary trees). All development steps are represented within a parameterized PVS theory which defines the required data structures and formalizes the application conditions by means of assumptions. Application (i.e., instantiation) of the steps is illustrated by means of simple examples. For example, we show how to correctly derive a mergesort program using divide-and-conquer. When applying a software development step the system automatically generates the necessary proof obligations which can be discharged using built-in and user-defined proof strategies.