The PROSPER Toolkit is based on HOL98, a modern descendent of the HOL theorem prover. HOL98 is highly modular, reflecting the project's approach to proof engine construction from components - whether HOL libraries or external plugins. It also has powerful and sophisticated automatic proof procedures. The system's command language is ML, a functional programming language extended with theorem proving functions and an implementation of higher order logic. This gives developers a full programming language to write custom verification algorithms and coordinate the invocation of plugins. Procedures programmed in a proof engine are offered to client applications in an API.

The toolkit includes the PROSPER Integration Interface, a set of libraries that implement a language-independent specification for communication between reasoning components. Implementations include libraries for Java, C, and ML. The toolkit also provides support to enable developers of other verification tools to offer them as PROSPER plugin components. Available plugins include a range of model-checkers and decision procedures, some developed by third-party researchers.

The latest public release of the toolkit is version 1.4. The system has been successfully built on recent versions of the Linux and Solaris operating systems.