定理证明( Theorem Proving )是最早的硬件形式验证的方法之一，其一般过程是：
　　第一步：将实现方案和功能描述都转换为一种形式逻辑，如命题逻辑、一阶逻辑(First-Order Logic, FOL)、高阶逻辑(Higher-Order Logic, HOL)等；
　　第二步：建立公理系统，作为验证的依据；
　　第三步：根据公理系统，用定理证明器，通过逻辑推理，逻辑规约等手段，构造证明过程，证明实现方案和功能描述等价。
　　定理证明的一个实例是由剑桥验证小组开发的HOL验证系统。HOL可以精确地描述和验证硬件，证明过程的每一步都十分严谨。但其缺点同其它基于定理证明或证明判别（Proving Checker）的方法一样：一个是证明过程十分冗长，即使一个最简单的证明也要很多步才能完成；另一个缺点则是不仅用形式逻辑来描述电路需要花费很大的精力，其证明过程也还需要大量的人工干预，这更是无法忍受的。
　　定理证明从原理上来说，并不难理解。有些研究所开发了定理证明器。证明的前提、目标等都与我们常见的定理证明一样。利用定理证明器，设计者应按照定理证明其的要求给出电路的描述和要证明的结论，输入计算机即可获得证明。因为定理证明器属于人工智能范畴，所开发的定理证明器所能证明的问题范围有限，因而还没有达到实用的地步，有时还需要人工对证明过程加以干预。