Zero-knowledge proofs enable selective disclosure of properties of secret data, but do not by themselves prevent information leakage through control flow or interaction structure. We present a choreographic programming model for zero-knowledge computation that integrates information-flow control at the language level. Our approach instantiates Pirouette’s local language with a core language with explicit proof construction and verification, and adapts the choreographic layer to make observable interaction structure explicit. We define a type system that enforces termination-insensitive noninterference, ensuring that secret data cannot influence publicly observable behavior except through explicitly verified proofs. Under standard idealized assumptions about zero-knowledge proofs, we prove a noninterference result for the local language. This work provides a foundation for writing zero-knowledge protocols that are secure not only in terms of cryptography, but also with respect to language-level information flow.

