The ground evaluator is an experimental feature of PVS that enables the animation of functional specifications. The ground evaluator extracts Common Lisp code from PVS functional specifications to evaluate ground expressions on top of the PVS underlying Common Lisp machine.

PVSio is a PVS package that extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. PVSio provides: An alternative (and simplified) Emacs interface to the ground evaluator; A user-friendly mechanism to define new semantic attachments; A stand alone (Emacs-free) interface to the ground evaluator; A set of proof rules that safely integrates the ground evaluator to the PVS theorem prover.