Model checking, the dominant formal verification method in hardware, verifies each design instance independently and returns only pass/fail. The proof reasoning stays locked inside solver heuristics and is reconstructed from scratch every run. CircuitProver breaks that pattern. It uses an LLM agent to translate parameterized hardware designs and natural language specifications into Lean 4 models, iteratively constructs machine-checked proofs through live Lean feedback, and then distills verified theorems and proving strategies into a reusable library. The next verification task that involves a related design can draw on accumulated lemmas instead of re-deriving them. Across 63 parameterized hardware benchmarks (adders, FIFOs, arbiters, and related structures), CircuitProver proves all of them. A vanilla agent without the library infrastructure solves 92.1% and requires twice as many proof rounds on average.
The mechanism that makes accumulation work is the library structure itself. Verified lemmas are parameterized, so a theorem proved for a 4-bit adder applies structurally to an 8-bit adder without re-proof. Proving strategies from past tasks guide agent reasoning on new ones. The ablation numbers quantify the savings: 16.3% shorter proofs and 23.2% faster verification time when the library is populated versus empty. These are not large absolute numbers, but the trend is compositional: the larger the family of related designs, the more the library pays off.
The verification bottleneck in advanced SoCs is not a lack of tools. It is that formal proof effort does not compound across design iterations. Every respin that touches an RTL block forces re-verification of properties that were already true. CircuitProver's approach argues that this re-proof cost is avoidable, and Lean 4 (a general-purpose proof assistant with a live checker) is a more durable substrate for accumulation than any EDA-specific formal tool. If this holds for module-level designs, the open question is whether it generalizes to hierarchical full-chip flows, where the majority of formal verification budget actually lives.