arxivcs.LOcs.AR2026-07-29
CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
Ziyi Yang, Wenji Fang, Chen Chen, Zhiyao Xie, Hongce Zhang
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 reason…