International Association
for Cryptologic Research

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 program’s internal logic. We propose a two-phase zero-knowledge protocol that hides program implementation details throughout verification. Phase I uses a zero-knowledge virtual machine (zkVM) to encode programs into SAT formulas without revealing their semantics. 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.