Like Coq or Isabelle, it is a proof assistant. It does not prove theorems automatically, but rather helps a user design coherent specifications, implement functions meeting those specifications, and prove theorems.

It is both a language and an inference system. The language is a typed higher order logic, featuring undecidable type checking.

One of the things I like about PVS is that type checking is undecidable. PVS will generate proof obligations (also called TCCs for Type Checking Conditions) from user theories, when it cannot fully type check these theories. PVS language is very flexible, as it allows the user write incoherent specifications or theories: unprovable TCCs will help the writer pin point mistakes, and gradually improve theories, without limiting user's creativity. This is a fruitful approach, very close to human reasoning. People, mathematicians, logicians do make mistakes: people need a tolerant framework, helping them find and correct their mistakes.