The NASA PVS Library is a collection of formal developments in PVS maintained by the NASA Langley Formal Methods Team and is part of the PVS research sponsored by NASA Langley.

The current version of the library is **NASA PVS Library 6.0.9 (11/10/14)** and
requires PVS 6.0.

- Basic distribution only includes specification and proof files.
- Classic distribution includes basic distribution and binary files.
- Full distribution includes classic distribution, the database utility Hypatheon 1.1, and pre-installed binaries of MetiTarski 2.2 and Z3 4.3.1 for Mac OSX 10.7.3 and higher and 64-bits Linux.

For quick installation, follow this instrutions. See installation notes for additional
details. For a list of updates, check `CHANGES.txt`

.
Furthermore, for PVS advanced users, the development version of the NASA PVS Library is available from
GitHub.

- Bernstein:
Formalization of multivariate Bernstein polynomials.
**Note**: The strategy`bernstein`

, which is available in PVS 5.0, is still no operational in PVS 6.0. - Hypatheon: A database capability for PVS theories.
- Interval: Formalization of interval arithmetic and strategies for numerical approximations and interval analysis(examples and more examples).
- MetiTarski/Z3: Integration of the theorem prover MetiTarski and SMT solver Z3 as external oracles to PVS (examples).
- Sturm: Formalization of Sturm's Theorem and strategies for proving univariate polynomial relations over a real interval (examples).
- Tarski: Formalization of Tarski's Theorem and strategy for proving systems of univariate polynomial relations on the real line (examples).
- Pre-installed in PVS:
- PVSio: Animation tool of PVS functional specifications (examples).

- For PVS 5.0 (including binaries, excluding binaries, installation notes).
- For PVS 4.2, PVS 4.1, PVS 4.0, PVS 3.3, PVS 3.2, PVS 3.1 (installation notes).