An integrated set of tools designed to aid in creating, analyzing, modifying, managing, and documenting program specifications and proofs. This methology includes a specification parser and type checker, a theorem prover, and a multi-level security checker. Note: This methodology is not based upon the Hierarchical Development Methodology.