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).
ProofLite has been part of PVS since PVS 5.0 and is included in the latest release of PVS.
ProofLite 6.0 provides:
*.pvs
files, e.g., prooflite_examples.pvs
.proveit
to re-prove theories in batch mode.provethem
to re-prove libraries (collection of theories) in batch mode.