PVS is now 15 years old, and has been extensively used in research, industry, and teaching. The system is very expressive, with unique features such as predicate subtypes, recursive and corecursive datatypes, inductive and coinductive definitions, judgements, conversions, tables, and theory interpretations. The prover supports a combination of decision procedures, automatic simplification, rewriting, ground evaluation, random test case generation, induction, model checking, predicate abstraction, MONA, BDDs, and user-defined proof strategies. In this paper we give a very brief overview of the features of PVS, some illustrative examples, and a summary of the libraries and PVS applications.