From Intent to Constraints: The Software Stack for ZK Computation

PhD Qualifying Examination


Title: "From Intent to Constraints: The Software Stack for ZK
Computation"

by

Mr. Zhantong XUE


Abstract:

Zero-knowledge (ZK) proof systems are usually presented through their 
cryptographic backends: proving schemes, polynomial commitments, and 
protocol-level efficiency. The deployed record locates the risk elsewhere. 
Over two thirds of catalogued real-world SNARK vulnerabilities arise not in 
the cryptography but in the software that translates high-level intent into 
circuits, constraints, and execution traces. This survey studies that 
translation layer: how programs and other semantic sources are represented, 
lowered, optimized, and checked before they reach a ZK backend. Proving 
systems themselves are outside its scope.

The survey organizes the ZK software stack into three frontend layers above a 
common backend interface. Layer 1 covers program-text frontends: circuit 
DSLs, higher-level ZK languages, and shared compiler infrastructures. Layer 2 
covers non-program frontends, whose source is a tensor graph, a relational 
query, or an automaton. Layer 3 covers zkVMs, which replace bespoke circuits 
with proofs of execution traces over fixed machine models such as RISC-V, 
WASM, the EVM, and Cairo. Across these layers it compares source 
abstractions, intermediate representations, and lowering pipelines, and 
catalogues the cross-cutting optimization methods, from constraint reduction 
and lookup-based encodings to quantization and proof-cost-aware compiler 
passes, together with the trust each demands.

Throughout, ZK compilation is treated as a correctness and security problem 
as much as a performance problem. Every frontend emits two coupled artifacts, 
a witness generator and a constraint system, and every gap between them is a 
potential failure of soundness, completeness, or zero knowledge. The survey 
derives a failure-mode taxonomy from these three guarantees: 
under-constrained circuits, over-constrained circuits, and leakage, produced 
by recurring causes such as witness--constraint inconsistency, missing range 
checks, unsafe hints, and compiler defects. Crossing these modes against the 
assurance techniques that claim to catch them (static analysis, SMT-based 
verification, refinement types, theorem proving, fuzzing, and metamorphic 
testing) yields a coverage matrix that shows where the stack is maturing, 
where reliability remains fragile, and which gaps must close before 
zero-knowledge computation can be trusted as ordinary software 
infrastructure.


Date:                   Tuesday, 28 July 2026

Time:                   3:00pm - 5:00pm

Venue:                  Room 3494
                        Lift 25/26

Committee Members:      Dr. Shuai Wang (Supervisor)
                        Dr. Dongdong She (Chairperson)
                        Dr. Lionel Parreaux