PVS (Prototype Verification System) is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.
The Allegro build requires agreeing to a license, so I cannot redistribute the sources. Hence, all you get here is a nosrc rpm.
Download the PVS 4.1 Allegro build for your platform (e.g., pvs-4.1-ix86-Linux-allegro.tgz).
This build only works on 32-bit platforms, due to the inherently 32-bit nature of both the BDD code in PVS and CMUCL itself. The resulting source RPM is bigger than I can manage on this web server (new web server coming soon; stand by!), so you'll have to put it together yourself from the pieces below.
Get the PVS 4.1 sources, and also unpack this set of patches.
Build with pvs-cmucl.spec.