“Open source library” is a very general concept. Most Coq projects are open source, and most are libraries, as opposed to plugins. If “library” is interpreted as system software, then many of the projects described in this thread may be of interest.
For the more narrow interpretation of standard utility library, see hs-to-coq, which verified many Haskell library functions. Outside of Coq and Haskell, CakeML has verified many standard utility functions (down to the processor ISA).