Zero-Knowledge Proofs for Verifiable AI Model Behavior

A zero-knowledge proof lets one party, the prover, convince another party, the verifier, that a particular statement is true, without revealing anything beyond the bare fact of that truth. The canonical illustration: proving you know a secret without saying what the secret is. The concept predates the AI industry by decades; its formal foundations trace to Goldwasser, Micali, and Rackoff in 1985. But what if the problem it was designed to solve had never arrived at scale? What makes it newly relevant is not that the mathematics changed, but that the problem it fits so precisely has finally arrived at scale.

Three properties define a valid ZK proof system. Completeness: an honest prover can construct a convincing proof. Soundness: a dishonest prover cannot fabricate one. Zero-knowledge: the proof leaks nothing about private inputs beyond the claim itself. These are not design aspirations. They are mathematically enforced guarantees, which is a different category of assurance than a contractual representation.

Apply that structure to the AI verification problem directly. The claim is: "I ran model X on your input and produced output Y." The secret is the model's weights. A ZK proof allows a provider to cryptographically certify that claim, with those three properties doing the work that trust currently does, without exposing the weights that represent years of proprietary investment. The math guarantees what the user cannot inspect and the provider cannot otherwise demonstrate.

I have spent enough time in cryptographic systems to appreciate how rarely a general-purpose tool fits a specific new problem this cleanly. Usually there is friction, a mismatch between what the primitive was designed for and what you are asking it to do. Here the fit is almost eerie. The AI verification problem asks for exactly what ZK proofs provide: a way to bind a computation to a commitment, publicly, without disclosure. The miracle, if you want to call it that, is that the mathematical infrastructure largely existed before anyone needed it for this.

How ZKML maps ZK cryptography onto machine learning computation

The intersection of zero-knowledge proofs and machine learning has a name now: ZKML. It has a recognizable origin point too. SafetyNets, published in 2017, was the first demonstration that a neural network prediction could be wrapped in a ZK proof at all. The models were small by current standards, and the performance was nowhere near practical deployment. But the existence proof mattered.

A 2025 survey by Peng et al. (arXiv:2502.18535), covering research from mid-2017 through mid-2025, organizes the field around three distinct verification tasks. Verifiable inference proves that a specific model with specific weights produced a given output from a given input. Verifiable training proves that training was performed correctly via declared gradient descent on declared data. Verifiable testing proves that a model meets a stated performance threshold without exposing model internals. Research has concentrated most heavily on inference verification, and the field's maturity reflects that. As Scaramuzza et al. (arXiv:2505.20136, May 2025) note, proving that a model was trained correctly on declared data is considerably harder than proving what it does on a given input, and the literature on training verification shows it.

The dominant proof systems in ZKML are zk-SNARKs and GKR-based interactive proof systems using the sum-check protocol. zk-SNARKs produce compact proofs suited for on-chain verification, where a third party needs to check the proof without any back-and-forth with the prover. GKR-based systems handle layered arithmetic computations well, which maps naturally onto the forward pass of a neural network.

For verifiable testing, the circuit construction follows a consistent pattern: public inputs include a cryptographic hash of model parameters, the test data and labels, a declared performance threshold, and a proving key; private witness inputs are the model parameters themselves. The circuit recomputes the parameter hash, checks consistency with the public hash, evaluates the model on the declared test set, and compares against the threshold. The model-as-commitment pattern is the conceptual anchor. Publishing a hash of the weights creates a public commitment; a subsequent ZK proof certifies that actual computation used weights matching that commitment, without exposing them. Once you see this structure, the elegance is hard to miss, even if the engineering underneath it is anything but elegant.

The arithmetic translation problem: floating point to finite fields

ZK circuits operate over finite fields, domains of modular integer arithmetic with no fractions and no approximation. Neural networks operate in floating-point arithmetic, specifically IEEE 754, which represents real values with fractional precision across an enormous range. These representations are fundamentally incompatible. Every multiply-accumulate in a linear layer, every weight and activation, must be translated into field operations before a ZK proof can be constructed over the computation. This translation problem is where most of the practical pain in ZKML lives.

The standard solution is quantization: approximating model weights and activations as fixed-point integers before circuit compilation. The accuracy penalty is real but bounded. For most benchmark tasks, quantization-induced accuracy loss falls in the 0.5 to 2 percent range. That tradeoff is manageable in many deployments. It is also worth considering, though, whether it is manageable in the applications that most urgently need proof. Safety-critical systems are the obvious case, and they are precisely the ones most likely to find even small accuracy penalties unacceptable. The field has not resolved this tension cleanly, and I would be skeptical of anyone who tells you otherwise.

Non-linear activation functions compound the problem. ReLU, Sigmoid, GELU, Softmax, Maxpooling, layer normalization: each introduces operations that do not translate natively into arithmetic circuits. Each requires a specialized circuit implementation. Current systems have achieved these implementations across the standard activation vocabulary, but the engineering effort is nontrivial and edge cases remain.

Attention mechanisms in transformers are the hardest translation problem in the current literature. The softmax-over-dot-products structure combines non-linearity, high dimensionality, and parallelism in a way that resists naive circuit encoding. zkLLM, published at ACM CCS 2024, introduced two targeted solutions: "tlookup," a parallelized lookup argument for non-arithmetic tensor operations that adds no asymptotic overhead, and "zkAttn," a specialized proof for the attention mechanism that balances runtime, memory, and accuracy. These are purpose-built constructions for a specific problem, not general solutions. That distinction matters because it illustrates just how granular the engineering challenges are at scale. Each layer of translation that seems solvable at small model size tends to reveal a new wrinkle at larger ones.

Where the research has reached and what it has proven possible

The trajectory from 2017 to 2025 is worth tracing as a sequence, because it shows both how far the field has moved and how the frontier keeps expanding rather than closing.

SafetyNets established ZKML as a concept and proved basic feasibility. zkCNN (ACM CCS 2021, Liu, Xie, and Zhang) extended ZK proofs to convolutional neural networks, covering both predictions and accuracy claims. Mystique (USENIX Security 2021, Weng et al.) addressed the efficiency of ZK conversions specifically for ML applications, improving practical viability beyond toy examples. Each of these papers solved a piece of the puzzle and in doing so revealed the next piece.

The ZKML optimizing system published at EuroSys 2024 (Chen, Waiwitlikhit, Stoica, and Kang) shifted focus from proof construction to system-level tractability, addressing the engineering problem of making ML inference in ZK circuits usable at meaningful scale. This was the pivot from "provably possible" to "possibly deployable," and it is worth marking.

zkLLM (ACM CCS 2024, Sun, Li, and Zhang) was the milestone paper for large language models. It demonstrated that LLM output authenticity verification is achievable in principle. The caveat: generating a proof for a single forward pass of Llama-2-13B took approximately 15 minutes on the reported hardware, against the milliseconds required for standard inference. That ratio is the central constraint the subsequent work has been trying to close, with incomplete success so far.

VeriLoRA (2025) addressed a practical gap the earlier work overlooked: verifying fine-tuned models. Most production LLM deployments are LoRA-adapted versions of base models, not base models themselves. Verification frameworks that cannot handle adapter layers have limited practical reach. VeriLoRA is the first ZK framework specifically addressing LoRA-based fine-tuning verification.

The Kaizen proof-of-training system applies GKR-style proofs to each gradient-descent iteration, then uses recursive composition to aggregate across iterations into a single concise proof. Training verification needs this kind of compression; individual-iteration proofs that cannot be aggregated become intractable at realistic training scales.

SVIP (2025, Sun et al., arXiv:2410.22307) targets verifiable inference for open-source LLMs, and ZKPROV (2025, arXiv:2506.20915) extends the verification perimeter upstream to training data provenance. The field is not one problem solved sequentially; it is a frontier expanding on multiple axes at once, which is exciting and, frankly, a bit disorienting from where I sit trying to track it.

What production systems can do in 2025

The shift from research demonstrations to deployed production infrastructure happened faster than most people outside the ZK community expected. I include myself in that category.

Lagrange Labs' DeepProve-1 is the first production zkML system to generate cryptographic proofs over a full LLM inference run on GPT-2. Compared to baseline EZKL for equivalent models, DeepProve-1 achieves proof generation approximately 1,000 times faster and verification approximately 671 times faster, with inference benchmarking improvements up to 700 times faster than existing solutions at that scale. DeepProve-1 is in active deployment across dozens of projects, with production use cases in healthcare, content moderation, and on-chain trading agents. Lagrange subsequently extended DeepProve to cover Google's Gemma 3 model, announced at a Verifying Intelligence event in Singapore hosted by House of ZK and Google Cloud.

zkPyTorch, released in March 2025, is a hierarchically optimized compiler that takes standard PyTorch models as input and compiles them directly to ZK circuits. VGG-16, a 138-million-parameter vision model, proves in 2.2 seconds under zkPyTorch. More importantly, ML engineers can now generate ZK proofs without any cryptography expertise. The tooling gap is closing alongside the performance gap, which matters considerably for adoption.

EZKL, developed by Zkonduit, converts ONNX model files to zk-SNARK circuits as an open-source library. Polyhedra Network's JSTprove, built on the Expander backend, supports ONNX models via an open-source toolkit for independent verification of AI model outputs. Modulus Labs has benchmarked proof systems for on-chain inference at models up to 18 million parameters.

The honest overhead picture for 2025: proving times range from seconds for simple classifiers to minutes for larger models on CPU hardware. GPU support, added across multiple systems in 2025, provides speedup factors ranging from single-digit multiples to roughly an order of magnitude. Real-time verified inference at full LLM scale is not yet practical. For models up to GPT-2 scale, it is, and that boundary has moved considerably in a short time.

The concrete situations where ZK verification changes what is possible

The substitution attack is the cleanest case to analyze. A cloud API user receives a ZK proof alongside the model's response, cryptographically binding the declared model to the declared output. Running a cheaper substitute and returning a proof for the claimed model is not merely detectable; it is mathematically impossible under a valid proof system. The economic incentive for substitution does not disappear. The feasibility does.

Regulatory compliance under the EU AI Act presents a structural tension that ZK proofs are well-positioned to address. The Act requires high auditability and verifiability for high-risk AI systems. Traditional compliance approaches, procedural audits, model documentation, are manual, expensive, and poorly matched to the opacity of large neural networks. Researchers have mapped existing ZKP solutions onto the EU AI Act framework; the ZKMLOps proposal outlines a modular process for generating cryptographic evidence that auditors can use directly for regulatory determinations. That raises an important question: can the law's demand for transparency and a provider's interest in confidentiality ever be satisfied at the same time? ZK proofs offer a structural answer — the regulator receives cryptographic evidence of the claim being audited; the provider retains confidentiality of the model that generated it. Both interests are preserved simultaneously rather than traded against each other.

The Laminator framework extends this logic to verifiable model properties. Providers can prove accuracy and fairness properties, combined with signed external certificates for dataset provenance, producing a model card that cannot be falsified after the fact. The current practice of self-reported model cards has no verification mechanism whatsoever, which is a problem hiding in plain sight.

Healthcare federated learning illustrates a different application of the same underlying logic. Multiple hospitals can collectively contribute to model training without sharing patient records; ZK proofs verify that each node followed the declared training protocol without exposing any patient information to the other participants. The privacy and verifiability requirements reinforce each other rather than pulling in opposite directions.

The defense deployment is the most striking current production case. Lagrange integrated DeepProve into Anduril's Lattice SDK, allowing every tactical decision in autonomous reconnaissance, including proximity detection, response classification, and movement calculation, to be cryptographically verified without revealing sensitive operational parameters. The military application strips away the commercial framing and gets at something more fundamental: verified AI behavior is about knowing, with mathematical certainty, what actually ran.

Backdoor and trojan detection round out the threat model. Research documented under NIST's TrojAI program demonstrates that models passing standard behavioral testing can embed malicious behaviors that activate only under specific trigger conditions. ZK-verified inference over declared model weights makes post-deployment modification detectable; if the weights change, the proof fails against the original commitment.

Worldcoin's World ID deployment is the largest-scale real-world ZKML application currently operating. The Orb device captures iris biometrics and generates a ZK proof verifying human uniqueness without retaining the underlying biometric data. Whatever one thinks of the broader Worldcoin project, the implementation demonstrates that ZKML is not a laboratory concept.

What remains hard and where the field's open problems sit

Proof generation overhead is the binding constraint. DeepProve-1 at GPT-2 scale is a production achievement. Llama-2-13B at 15 minutes per forward pass is a research demonstration. The distance between those two points is not a rounding error; it is the field's central open problem, and closing it requires hardware, software, and algorithmic progress simultaneously. GPU proving helps. It does not close the gap to real-time at LLM scale, and anyone suggesting otherwise is being optimistic in ways that should prompt follow-up questions.

Training and data preprocessing verification remain the least mature areas. Scaramuzza et al. (arXiv:2505.20136, May 2025) identify this explicitly. Proving inference over declared weights is increasingly solvable in practice. Proving that the training process was faithful to its declared protocol is harder: training involves more operations, longer time horizons, stochastic elements, and data dependencies that resist encoding in arithmetic circuits. The Kaizen approach points in the right direction. The engineering work is substantially incomplete.

Quantization accuracy loss is bounded but not zero. For applications where small systematic errors are consequential, the ZK-provability tradeoff may not be acceptable at current quantization levels. This is not a fundamental impossibility in the theoretical sense, but it is an unsolved engineering problem for the highest-stakes applications, which are precisely the ones that should most want proofs.

Hardware cost creates adoption asymmetry. Proof generation at inference speed requires significant compute, even with GPU support. Well-funded organizations can absorb this. Smaller operators cannot. If ZK verification becomes a compliance requirement without a corresponding reduction in proving costs, the compliance burden falls unevenly in ways that may entrench incumbents while nominally improving the field.

Composability at scale is an open problem. Verifying a single model's behavior on a single input is now solved in principle. Verifying a multi-model pipeline, an agent architecture where each model's output feeds another's input, introduces combinatorial complexity that current frameworks do not handle cleanly. Cysic has announced verifiable multi-agent swarms on mainnet, but the infrastructure for composable ZK verification across complex agent architectures does not yet exist in a mature form. I am watching this space with interest and some skepticism.

Standardization is absent, and the absence is starting to matter. Proof formats, circuit conventions, and verification interfaces differ across EZKL, Polyhedra's tooling, Lagrange's DeepProve, and circomlib-ml. No interoperability layer exists. A ZK proof generated by one system cannot be checked by another. This is a coordination problem rather than a technical impossibility, but coordination problems have their own inertia, and the field has not yet found its way to a shared protocol.

One more thing, because it is easy to miss in the enthusiasm: a ZK proof certifies computational faithfulness. It proves that the declared model ran the declared computation and produced the declared output. It does not prove that the output is correct in any substantive sense. A model can produce a verifiably authentic ZK proof and still give wrong, biased, or harmful answers. But how does this affect our original promise? The proof guarantees the integrity of the computation. Whether the underlying model is fit for purpose is a separate question entirely, and ZK does not touch it.

What cryptographically verifiable AI behavior means for how trust gets structured

The trust model that currently governs AI services is a version of institutional faith. Users rely on provider reputation, contractual terms, and the general presumption that large commercial operators will not systematically deceive them. This has historically been sufficient for many software services. It is increasingly insufficient for AI systems making consequential decisions, because the gap between claimed and actual behavior is now technically invisible rather than merely difficult to inspect.

ZK verification relocates trust from providers to mathematics. The properties of a ZK proof system are formally defined and publicly auditable; once you accept the mathematical foundations, individual proof verifications require no judgment about provider credibility. For people who work in security and have spent years watching "trust us" fail in various spectacular ways, this is not a minor improvement. It is a structural change in the relationship.

For regulated industries, the implications are concrete. A compliance officer currently faces a choice between demanding transparency that exposes proprietary IP and accepting opacity that may conceal non-compliance. ZK proofs dissolve that binary. The regulator receives cryptographic evidence of the claim being audited; the provider retains confidentiality of the model that generated it. Both interests are satisfied structurally rather than balanced against each other through negotiation, which is a different and more durable kind of resolution.

For individual users, ZK proofs represent the first mechanism that makes "trust but verify" technically meaningful rather than aspirational language. The ability to verify does not require understanding the cryptography. It requires only that the proof verification step exists in the infrastructure and that its result surfaces in a form the user can act on. This is an interface and tooling problem as much as a cryptographic one, and the cryptography is the easier part.

The field is early. Production systems exist for models up to GPT-2 scale with full proof generation. Research systems have demonstrated feasibility at LLM scale with performance characteristics that are not yet practical for real-time deployment. The engineering gap is closing faster than the standardization gap. I do not know whether the horizon at which ZK verification becomes a baseline expectation for consequential AI deployments arrives in three years or ten or longer, and I am suspicious of anyone who claims to know. What I find harder to argue, looking at the research trajectory and the production deployments already operating, is that it does not arrive at all. The mathematical foundations are solid. The engineering is moving. The demand is obvious. That combination has a way of resolving itself, eventually, into infrastructure.