As AI agents become more capable of generating and optimizing hardware circuits, guaranteeing the correctness of AI‑generated designs grows increasingly important. At the same time, advances in AI lower the entry barrier for formal methods, opening new possibilities for automating hardware verification. This invited paper surveys the main methodologies and applications of hardware formal methods in the AI era. First, it examines how agentic AI advances formal methods at three levels: specification, proof construction, and reasoning engines. Second, it describes how formal methods support reliable AI‑driven hardware development through RTL generation, debugging, and correctness‑preserving optimization, highlighting representative studies and our recent contributions that reveal key technical advances and experimental insights. Finally, it looks ahead to proof‑native hardware development, where formal reasoning becomes an integral part of autonomous hardware design.\n\nReview: The article provides a comprehensive roadmap linking AI and formal verification, offering a solid foundation for building trustworthy autonomous hardware.