I think AluoNowu was referring to the last line of the abstract in this paper: http://www.usenix.org/events/nsdi04/tech/full_papers/musuvathi/musuvathi_html/main.html, which reads: We have implemented these techniques in CMC, a C model checker [30] and applied the result to the Linux TCP/IP implementation, finding four errors in the protocol implementation. What bugs were there would surely by now have been fixed...