PVS Specification and Verification System
The PVS Specification and Verification System is a verification system: that is, a specification language integrated with support tools and a theorem prover. The latest version (4.0) works best with ACL 8.0 (should work with version >= 6.2). CMUCL 19c is also supported.

As of version 4.0 (november 2006) PVS is now distributed under the terms of the GPL licence.

Theorem Provers