随着 AI 代理在硬件电路生成与优化方面的能力不断提升，确保 AI 生成设计的正确性变得尤为关键。与此同时，AI 技术的进步降低了形式化方法的使用门槛，为硬件验证的自动化提供了新契机。本文概述了硬件形式化方法在 AI 时代的主要方法论与应用。首先，分析了 agentic AI 如何在规范、证明构造和推理引擎三个层面推动形式化方法的发展。其次，阐述了形式化方法在 RTL 生成、调试以及保持正确性的优化过程中的支撑作用，并结合代表性研究与我们近期的工作展示了关键技术进展与实验洞见。最后，展望了面向证明原生硬件开发的未来方向，即让形式化推理成为自主硬件设计的内在环节。\n\n点评：本文系统梳理了 AI 与形式化验证的交叉路径，为实现可靠的自主硬件提供了清晰的技术路线图。