PVS is a proof assistant/mechanized environment for formal specification and verification developed at SRI International. It was first described in a 1992 paper at CADE, and first released in 1996 (according to the website).
For many years the PVS project has enjoyed the support of the NASA Langley Formal Methods Research Programme.
PVS is still in active development as of 2021. For example, there is even a VSCode plugin.
To the best of our knowledge, PVS is also the only verification system to have featured in a film.
The presentation here originates in the PVS documentation.
PVS is based on classical, typed higher-order logic. The base types include uninterpreted types that may be introduced by the user, and built-in types (booleans, integers, reals, etc.).
Predicate subtypes and dependent types can be used to introduce constraints, such as the type of prime numbers or order-preserving maps.
The theorem prover itself consists of interactive application of rules of a sequent calculus.
The rule application routines (called primitive inferences) are optimised for large proofs: for example, propositional simplification uses BDDs, and auto-rewrites are cached for efficiency. User-defined procedures can combine these primitive rule applications to yield higher-level proof strategies.
Original paper at CADE 1992:
Owre, S., Rushby, J.M., Shankar, N. (1992). PVS: A prototype verification system. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_217