We routinely run nbdkit through Coverity and it finds bugs, although it too has false positives. Also the reports produced by Coverity are really nice - long enough to tell you where the bug is, but not too long to be overwhelming.
I've been meaning to formally prove one of our internal "mini libraries" using Frama-C. If we did that then no one would be able to complain about bugs in it :-)
