EZKL is a library and command-line tool from the company Zkonduit for proving neural-network inference in zero knowledge.
It compiles a model exported in the ONNX (Open Neural Network Exchange) format into a halo2 circuit, quantizing its values, so a prover can show that a model produced an output without revealing whichever of the model or the data is private. Its source code is public. A 2025 audit by the security firm Trail of Bits found proof-forgery bugs in its circuits and smart contracts, and all high-severity ones were fixed.
Trail of Bits reports that other projects use its verifier contracts in production. Its main limit for AI verification is scale: the largest language model in South et al.'s published results is a 250,000-parameter nanoGPT, which took 46 minutes to prove with a 219 GB proving key. Quantization also leaves a gap between the proven circuit and the full-precision model.
Public, independently audited code proves small models against a cheating prover, but its published results stop far below the size of the language models that verification claims concern.
Assessed use: proving a language model's output follows from committed weights, against a cheating prover
On this page
What it is
EZKL ("Easy Zero-Knowledge Inference") is a library and command-line tool for proving neural-network inference in zero knowledge, developed by Zkonduit 1. It supports statements such as "I ran this publicly available neural network on some private data and it produced this output", and the converse with a private model and public data 1. It implements zero-knowledge proofs of inference.
How it works
EZKL takes a model exported in the ONNX format, for example from PyTorch or TensorFlow, and turns it into a circuit for the halo2 proof system 1. Operations are quantized on the way, so EZKL's outputs can differ slightly from the original model's 1. A verifier checks the resulting proof natively or through a smart contract on a blockchain 3.
South et al. use EZKL to bundle proofs over a dataset into an attestation that a model with fixed private weights reaches a stated score on public inputs 2.