As of version 4.0 (november 2006) PVS is now distributed under the terms of the gpl licence.
Previous versions are available free-of-charge for non-commercial use only, which technically makes them non-free. The web site for PVS explains the capabilities and licensing terms for the system.
CLiki pages can be edited by anyone at any time. Imagine a fearsomely comprehensive disclaimer of liability. Now fear, comprehensively