Theorem proving is a technology where we use logical deduction to prove properties of mathematical artifacts, often assisted by a computer program called a theorem prover. One way to verify computing systems is to model them as mathematical artifacts and then use theorem proving to prove their desired properties as theorems. This approach has in fact been used to verify a wide spectrum of properties of computing systems. In this chapter, we recount the role of theorem proving in microprocessor verification and discuss the scope, applicability, and limits of the technology.