ProofLite is a tool for non-interactive proof checking in PVS. ProofLite also enables a semi-literate proving style in PVS where specification and proof scripts reside in the same file (as it is done in Coq and other proof assistants). See INSTALL for installation instructions, and the directories examples/ and doc/ for examples and documentation, respectively.