Penelope is a prototype system for interactively developing and verifying programs that are written in a rich subset of sequential Ada. Penelope can be used to develop a program and its correctness proof incrementally, and in concert with one another. Incrementality is used in a number of ways to help make verification more tractable and more productive. For example, if an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original verification.
Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. Larch/Ada scales up properly, in the sense that it is demonstrably sound to decompose a system hierarchically and reason locally about the implementation of each piece.
Penelope has been applied in various demonstration projects---for specification (guidance control, distributed operating system), verification (of off-the-shelf code), and formal development (by non-expert as well as expert users). Some features of Penelope have been embodied in AdaWise, a lint-like non-interactive tool that warns of the potential for certain dynamic semantic errors in Ada programs.