Search papers, labs, and topics across Lattice.
This paper introduces CircuitProver, a Lean 4-based framework that automates the verification of complex integrated circuits by translating parameterized hardware designs and their specifications into executable models. By leveraging proof-accumulation and reusable proof artifacts, CircuitProver significantly reduces the effort required for formal verification and enhances the efficiency of the proving process. The results demonstrate that CircuitProver successfully proves all tasks in a benchmark suite, outperforming a vanilla agent in both proof success rates and efficiency, with notable reductions in proof length and verification time.
CircuitProver not only automates hardware verification but also distills proof knowledge into reusable libraries, slashing verification time by over 23%.
Modern integrated circuits (ICs) are becoming increasingly complex, making functional verification a major bottleneck. The dominant hardware formal verification methodology, model checking, verifies each design instance separately and exposes only pass/fail results, so the reasoning behind a proof stays locked inside solver heuristics and is repeatedly reconstructed across related designs. Interactive theorem proving instead yields explicit, reusable proof artifacts, but applying it to hardware remains largely manual, demanding expert effort for formalization, invariant discovery, and proof development. In this paper, we present CircuitProver, an agentic Lean 4-based verification framework supporting proof-accumulation and parameterized verification. CircuitProver automatically translates parameterized hardware designs and their natural language specifications into executable Lean 4 models. It then iteratively constructs machine-checked proofs through Lean feedback to establish that the hardware code complies with the specification. The proving traces and verified theorems are distilled into reusable libraries, where proving strategies guide future agent reasoning and verified lemmas support formal proof reuse across related hardware verification tasks. We further introduce the first benchmark suite for evaluating agentic hardware theorem proving, covering diverse parameterized hardware designs, specifications, proof tasks, and evaluation metrics. Across 63 tasks, CircuitProver successfully proves all benchmarks, while a vanilla agent solves 92.1% of them and requires twice as many proof rounds on average. Ablation studies show that accumulated proof knowledge reduces redundant proof construction across related verification tasks, reducing proof length by 16.3% and verification time by 23.2%.
