[rwmj]

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 :-)