Hongce Zhang

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…Read more