ZK-ProVer: Proving Programming Verification in Non-interactive Zero-Knowledge Proofs

doi:10.1007/978-981-95-4213-0_12

Return

ZK-ProVer: Proving Programming Verification in Non-interactive Zero-Knowledge Proofs

2026-01-01

PRE

DOI：10.1007/978-981-95-4213-0_12

Original

Original request for help

Save

Abstract

En 中文

Program verification ensures software correctness through formal methods but incurs substantial computational overhead. It typically encodes program execution into formulas that are verified using a SAT solver and its extensions. However, this process exposes sensitive program details and requires redundant computations when multiple parties need to verify correctness. To overcome these limitations, zero-knowledge proofs (ZKPs) generate compact, reusable proofs with fast verification times, while provably hiding the programs internal logic. We propose a two-phase zero-knowledge protocol that hides program implementation details throughout verification. In Phase I, a zero-knowledge virtual machine (zkVM) is employed, which adopts HyperPlonk as the underlying protocol. This zkVM enables the encoding of programs into Boolean Satisfiability (SAT) formulas, while strictly avoiding the disclosure of the programs' semantic information. Phase II employs the encoding of resolution proofs for UNSAT instances and circuits for satisfying assignment verification for SAT instances through PLONKish circuits. Evaluation on the Boolector benchmark demonstrates that our method achieves verification time that is efficient and is independent of clause width for UNSAT instances and formula size for SAT instances. The resulting ZKPs enable efficient verification of program properties while providing strong end-to-end privacy guarantees.

Keywords:

program verification

zero-knowledge proofs

SAT

PLONKish

zkVM