You can't have a bug in the proof library, or the proof-checker won't accept your proof as true! You can have a bug in the proof-checking kernel which makes it accept false theorems, but that's precisely why we keep proof-checking kernels as small and well-debugged as possible, sometimes going so far as to formally verify them too (Coq in Coq[1]).

[1] http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf