CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
This paper presents CircuitProver, an agentic Lean 4-based verification framework supporting proof-accumulation and parameterized verification, and introduces the first benchmark suite for evaluating agentic hardware theorem proving, covering diverse parameterized hardware designs, specifications, proof tasks, and eval...