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 license.

Repository: https://github.com/SRI-CSL/PVS

Theorem Provers