현대의 집적 회로 (ICs)는 점점 더 복잡해지고 있으며, 이로 인해 기능 검증 (functional verification)이 주요 병목 현상이 되고 있습니다. 지배적인 하드웨어 형식 검증 (formal verification) 방법론인 모델 체킹 (model checking)은 각 설계 인스턴스를 개별적으로 검증하고 통과/실패 결과만을 노출하므로, 증명 뒤에 숨겨진 추론 과정이 솔버 휴리스틱 (solver heuristics) 내에 갇혀 있게 되며 관련 설계 전반에 걸쳐 반복적으로 재구성되어야 합니다. 반면, 대화형 정리 증명 (Interactive theorem proving)은 명시적이고 재사용 가능한 증명 산출물을 생성하지만, 이를 하드웨어에 적용하는 것은 형식화 (formalization), 불변량 발견 (invariant discovery), 증명 개발을 위해 전문가의 노력을 요구하는 등 여전히 상당 부분 수동적인 상태로 남아 있습니다. 본 논문에서는 증명 축적 (proof-accumulation)과 매개변수화된 검증 (parameterized verification)을 지원하는 에이전트 기반 Lean 4 기반 검증 프레임워크인 CircuitProver를 제시합니다. CircuitProver는 매개변수화된 하드웨어 설계와 그 자연어 사양 (specifications)을 실행 가능한 Lean 4 모델로 자동 변환합니다. 그런 다음 Lean 피드백을 통해 기계 검증된 증명을 반복적으로 구축하여 하드웨어 코드가 사양을 준수함을 입증합니다. 증명 추적 (proving traces)과 검증된 정리 (verified theorems)는 재사용 가능한 라이브러리로 추출되며, 여기서 증명 전략은 향후 에이전트의 추론을 가이드하고 검증된 보조정리 (lemmas)는 관련 하드웨어 검증 작업 전반에서 형식적 증명 재사용을 지원합니다. 나아가 우리는 다양한 매개변수화된 하드웨어 설계, 사양, 증명 작업 및 평가 지표를 아우르는 에이전트 기반 하드웨어 정리 증명 평가를 위한 최초의 벤치마크 제품군을 도입합니다. 63개의 작업에 대해 CircuitProver는 모든 벤치마크를 성공적으로 증명한 반면, 일반적인 에이전트 (vanilla agent)는 그 중 92.1%를 해결하며 평균적으로 두 배 더 많은 증명 라운드 (proof rounds)를 필요로 했습니다. 절제 연구 (Ablation studies)에 따르면 축적된 증명 지식은 관련 검증 작업 간의 중복된 증명 구축을 줄여, 증명 길이를 16.3% 단축하고 검증 시간을 23.2% 감소시킵니다.