We have implemented several PVS libraries over the years, at LaBRI and ENSEIRB-MATMECA: some of them are general purpose; others are more like illustrative examples PVS specification and proof. Students have also contributed, on academic projects. One of the difficulty is to maintain compatibility with new PVS releases. We are presenting some examples here, with the aim of gradually offering more!
More examples in the world of PVS users
These are referenced by PVS wiki (which is not very active), but there are (or have been) a lot more users, who have developed substantial libraries in various domains.