Abstract: This paper introduces the formal verification techniques for hardware designs using HOL (Higher-Order Logic) system. The implementation of a temporal logic in top level of HOL is described, and an example of verifying a latch using this mechanized temporal logic is given.