Verified computation techniques enable the construction of zero-knowledge proofs that an output was computed by a particular program—without revealing the program's input. Existing techniques work by converting programs into circuits or constraints, which makes dealing with control flow challenging. We present a new approach that compiles the program to a specialized abstract machine that contains no control flow and is particularly well-suited to zero-knowledge proof.