Recent announcements are posted here, a complete list, including future plans are on the Status page.

• November 21, 2006: PVS 4.0 (open source) released -
  PVS 4.0 is available, see the download page for details.
• May 24-27, 2005: NASA Langley - NIA training course on PVS
  The Formal Methods teams at NASA Langley Research Center and the National Institute of Aerospace are offering a short course on PVS in the spring of 2005. The class will take place May 24-27 in Hampton, Virginia. We have conducted this course several times in the past, most recently in April 2003. Our policy is to offer the course free of charge as a public service to the technical community. In return, attendees bear the cost of traveling to our site. The class is open to all interested individuals, including non-US citizens. See the link above for details and registration information.
• November 29, 2004: Release of PVSio.2a.
  PVSio is a PVS package that extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. The PVSio library is implemented via semantic attachments.
  PVSio is freely available at http://research.nianet.org/~munoz/PVSio/
  Send comments and user reports to César Muñoz.
• November 10, 2004: NASA PVS libraries for PVS 3.2.
  The NASA PVS libraries have been updated to PVS 3.2. This consists of the libraries algebra, analysis, calculus, complex, digraphs, fixedpoints, graphs, ints, lnexp, number_theory, reals, series, sets_aux, structures, trig, trig_fnd, and vectors.
  They are freely available at
  http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
  or directly from
  http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/p32_pvslib-full.tgz
  Send comments and user reports to Rick Butler
• November 4, 2004: PVS 3.2 released.
  See the download page for details.
• January 9, 2004: ProofLite Package for PVS 3.1.
  ProofLite is a library package for non-interactive proof scripting in PVS. It allows for a literary 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 is also suitable for automatic or batch generation of specifications and proof scripts.
  ProofLite is freely available at: http://research.nianet.org/~munoz/ProofLite/
  Send comments and user reports to César Muñoz.
• February 18, 2003: Manip 1.1 and Field.2a.
  The prover strategy packages, Manip and Field, are now available for PVS 3.1. Both offer enhanced automation for arithmetic deduction. Manip carries out user-directed manipulation steps. Field works with Manip to achieve higher level simplification. Both packages exploit new 3.0/3.1 features for loading libraries, making installation simpler and more robust.
  You may retrieve these libraries directly:
  • Manip 1.1
  • Field.2a
  Send comments and user reports to Ben Di Vito and César Muñoz.
• February 14, 2003: PVS 3.1 released.
  See the announcement for details, and go to the download page to get the new image and documentation.