Protecting the confidentiality of hardware designs is essential, especially during third-party verification, where proprietary designs must be examined by potentially untrusted verifiers. Existing approaches, such as obfuscation, watermarking, design encryption, and prior privacy-preserving verification techniques, are either not applicable, rely on trusted third parties, or lack scalable formal guarantees.

We present ZSafe, the first zero-knowledge (ZK) framework to provide formal safety guarantees for proprietary hardware designs. ZSafe enables a designer to prove the safety of confidential hardware to a verifier without revealing the design. Our approach introduces (i) an encoding scheme for hardware design, and a ZK-friendly constraint system that binds hardware design and its formula representation, (ii) an efficient ZKP protocol for validating logical implication, avoiding the prohibitive overhead of formula translation by using probabilistic checking, and (iii) a shared-structure unsatisfiability proof protocol to handle interrelated verification checks efficiently. We implement ZSafe and evaluate it on 69 adapted HWMCC’24 benchmarks with up to 300,000 gates. The results demonstrate practical scalability: 90% of instances are proven within an hour, with orders-of-magnitude improvements over prior approaches.