Prototype Verification System

The Prototype Verification System (PVS) is a specification language integrated with support tools and an automated theorem prover, developed at the Computer Science Laboratory of SRI International in Menlo Park, California.

Type-constructors include functions, sets, tuples, records, enumerations, and abstract data types.

Predicate subtypes and dependent types can be used to introduce constraints; these constrained types may incur proof obligations (called type-correctness conditions or TCCs) during typechecking.

PVS specifications are organized into parameterized theories.

The system is implemented in Common Lisp, and is released under the GNU General Public License (GPL).