Ensuring that a design conforms to its specification is an indispensable part of the modern design automation flow. Model checking is an automated verification technique for checking whether a given system satisfies a desired property. This problem has received much attention in the theoretical and practical domains from both industry and academia. In this chapter, we describe some of the most important contributions made to bit-level model checking, which made it an essential tool used by hardware design companies during the development process of modern hardware designs.