Zero-knowledge proofs (ZKPs) are computationally demanding to generate. Their importance for applications like ZK-Rollups has prompted some to outsource ZKP generation to a market of specialized provers. However, existing market designs either do not fit the ZKP setting or lack formal description and analysis. In this work, we propose a formal ZKP market model that captures the interactions between users submitting ZKP tasks and provers competing to generate proofs. Building on this model, we introduce $Proo\varphi$, an auction-based ZKP market mechanism. We prove that $Proo\varphi$ is incentive compatible for users and provers, and budget balanced. We augment $Proo\varphi$ with system-level designs to address the practical challenges of our setting, such as Sybil attacks, misreporting of prover capacity, and collusion. We analyze our system-level designs and show how they can mitigate the various security concerns.