InfiniVerif: Closing the Trust Gap in Agentic Hardware Design via Fully Automated Formal Verification

Large Language Models (LLMs) are accelerating chip-design workflows by reducing manual RTL coding and shortening design iterations. However, agent-generated RTL must be rigorously verified, while manual verification cannot keep pace with agentic code generation. Asking an agent to generate testbenches or assertions only transfers the trust problem to another artifact that may itself contain hallucinations. This is the Trust Gap between rapid RTL generation and establishing correctness before fabrication. We present InfiniVerif, an automated workflow for formal RTL verification and debugging. Formal verification checks stated properties exhaustively under explicit assumptions. InfiniVerif translates unmodified Verilog and target properties into Lean~4, where an LLM constructs the invariants and proof steps for an interactive-theorem-proving workflow and Lean's kernel deterministically checks every accepted proof term. Structure-preserving translation, data-plane semantic lifting, and cyclic collapse reduce the complexity of sequential proof obligations. Failed obligations and counterexamples guide RTL repair, while re-verification after an RTL change takes minutes. We validate InfiniVerif on a five-stage MIPS pipeline, the lowRISC Ibex instruction cache, and the Spatz vector processor. The workflow proves arbitrary-length ISA equivalence, cache transparency and deadlock freedom, and repairs latent control-hazard and divider-scheduling bugs. Under the evaluated configurations, bounded model checking, $k$-induction, and IC3/PDR fail to discharge the corresponding properties, demonstrating the scalability of our approach for an efficient and trustworthy end-to-end agentic hardware design flow.