PVS is a mechanized environment for formal specification and verification. PVS consists of a specification language, a large number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples that illustrate different methods of using the system in several application areas. By exploiting the synergy between a highly expressive specification language and powerful automated deduction, PVS serves as a productive environment for constructing and maintaining large formalizations and proofs. See the description page for a summary of the features of PVS, and the documentation page for full details.
PVS builds on over 40 years of experience at SRI in developing and using tools to support formal methods. See fm.csl.sri.com for a description of formal methods at SRI, and some of our formal methods tools.
PVS has had many contributors over the years, but would probably not even exist without the continuing support and encouragement from the NASA Langley Formal Methods Research Program. They have been with us from the beginning, and have put together a huge library of PVS theories that are freely available. It is highly recommended that you download and use these, both as libraries and as examples of complex PVS specifications and proofs. Many of the tools currently in PVS were developed by this group. Check out the link for details on PVS related research sponsored by NASA. There you can even learn about how the NASA PVS Library was featured in the movie "The Martian"
PVS 7.1 (release notes) is the current stable version of the tool. There are free versions for Linux and Mac, for both Allegro and SBCL Common Lisp. Allegro has more features, and is generally quite a bit faster, but requires acceptance of a click-through license. If you are a commercial entity and you don't already have a PVS license (any version), or have licensing questions, please contact us at pvs-licensing@csl.sri.com
PVS sources are available on Github.
