The canonical taxonomy of verifiable machine learning has three objectives, and ZKP-VML Survey states it in as many words:

Depending on the stage of the ML pipeline being certified, verifiable machine learning can be divided into three primary categories: Verifiable Training, Verifiable Testing, and Verifiable Inference.

ZKP-VML Survey · §II-C, Verifiable Machine Learning

Note the axis it slices on: the stage of the pipeline being certified. Training, then testing, then inference, one bucket per stage, and every bucket contains proofs that a computation was performed as declared. It is a good taxonomy and it exhausts its axis.

The systems on this page do not fit it, and the reason is not that they are a fourth stage. It is that they are not about a stage at all. They prove a property of the artefact rather than the correctness of a process. "This model does not discriminate against a protected group." "These weights were derived from data I was licensed to use." "This provider is not censoring outputs for some users." None of those is a statement about whether a matmul was computed correctly, and you cannot reach any of them by proving harder that one was.

We treat that as a fourth verification objective. It is the one place where this SoK departs structurally from the surveys it builds on, see Surveys for the other two departures.

Why it genuinely does not reduce to the other three

The obvious objection is that a property proof is just an inference proof wearing a hat: to prove fairness, run the model on a dataset and prove the outputs satisfy a predicate. That works, and it is what the first generation of these systems did. It also does not scale, and, more importantly, it proves the wrong thing.

It does not scale, because a property of a model quantifies over inputs, while a proof of inference is about one input. Proving a group-fairness property by inference means proving inference over an entire evaluation set, and the cost is the cost of the whole inference section multiplied by the size of the set.

FairZK is the system that breaks this, and the unlock is conceptual rather than cryptographic: it derives fairness bounds from the model parameters plus aggregated input statistics, rather than by proving inference over a specific dataset. That is a different mathematical object, a bound on the model's behaviour, not a transcript of its behaviour, and it is why FairZK reaches a parameter count that inference-based fairness proofs cannot (see the table).

It proves the wrong thing, because a property proved on a dataset is a property of the dataset as much as of the model. Prove fairness on the evaluation set and a malicious provider will hand you a model that is fair on the evaluation set. OATH is the system that takes this seriously: it targets online group fairness, fairness on the traffic the model actually serves, under distribution shift and under provider malfeasance, using a cut-and-choose protocol over statistical properties of the fairness definition, with a ZK proof of correct inference as a subroutine rather than as the whole mechanism. Note what that composition says: property proofs sit on top of the inference systems in this SoK. They are not a competing cell; they are a consumer of one.

The problem that does not go away

Here is the thing an auditor has to hold onto, and it is not a cryptographic problem, so no amount of cryptography will fix it.

A proof that a model is fair is only as good as the definition of fairness it encodes, and that definition is contestable in a way that "this matmul was computed correctly" is not.

Correctness has a referent. There is a fact of the matter about what $A \times B$ is, the prover and verifier agree on it in advance, and a soundness bug is a discrepancy against that fact. Fairness has no such referent. It has a literature, demographic parity, equalized odds, predictive parity, individual fairness, counterfactual fairness, whose central results include the impossibility theorems establishing that the major group-fairness criteria cannot in general be satisfied simultaneously. Choosing one is choosing a side in a normative argument, and it is a choice the prover is making when they write the circuit.

So the security property degrades in a specific and predictable way. A sound ZK proof of fairness gives you:

The provider ran a computation which, if the predicate encoded in this circuit is the right notion of fairness, and if the protected-attribute labels fed to it are honest, establishes that this model satisfies it on this distribution.

Every clause in that sentence is a place to attack, and only the first one is cryptographic.

This is not a reason to dismiss the work, it is a reason to read it correctly. The cryptography is doing something real: it lets a provider demonstrate a property while keeping the model confidential, which is the only reason this is hard at all. Absent confidentiality, an auditor would just be given the weights. The proof is buying confidentiality, not objectivity, and it is worth being precise that those are different purchases.

Provenance is the more tractable half

The fairness systems get the attention; the provenance ones may end up mattering more, precisely because they do have a referent.

"These weights were derived from this committed dataset" is a claim with a fact of the matter, exactly like "this matmul was computed correctly." There is no contestable definition in the middle. And it is the claim that copyright litigation, licensing compliance, and the EU AI Act's data-governance provisions actually turn on.

zkAudit is the most complete system here and it straddles both. Its first phase, ZKAudit-T, proves the model was trained by SGD on a committed dataset, that is a zero-knowledge proof of training, and it cross-lists into the training section. Its second phase, ZKAudit-I, then audits arbitrary user-defined properties over the hidden data and weights: copyright, censorship detection, counterfactuals. The layering is the right architecture, pin the artefact first, then interrogate it, and it is why zkAudit supports property audits that the fairness systems' narrower approach cannot express.

zkAudit also makes a design choice with consequences well beyond this page: the weights stay secret but the architecture is public. That is exactly the mitigation the Fiat–Shamir/GKR question turns on. A system that pins its architecture is a system whose prover did not get to choose its circuit.

ZKPROV is the cheap version of the same idea, prove which dataset a model was trained on, without proving the training computation at all. Weaker claim, far weaker cost, and for a licensing dispute it may be the entire claim anyone wanted.

The system-level end of the spectrum

Two entries reach past the model to the thing the model is embedded in, and we have read neither, so they are listed rather than assessed. Show Me You Comply audits an AI-enabled system for regulatory compliance rather than auditing a model. And Cryptographic Verifiability of E2E AI Pipelines frames data ingestion, training and inference as a single verifiable pipeline, which is, in effect, the argument that the three-objective taxonomy should be replaced by one continuous chain of custody rather than extended by a fourth bucket.

The people are the same people

Worth noticing, because it explains why these clusters share techniques. FairProof is Yadav, Roy Chowdhury, Boneh, Chaudhuri, Roy Chowdhury also wrote EIFFeL, and Boneh co-authored Prio, both in federated aggregation. FairZK includes Yupeng Zhang, who co-authored zkCNN and DeepProve. zkAudit comes from the group behind ZKML.

The verifiable-FL, zkPoT, inference and property-proving clusters are not four communities. They are one community, working four problems, and the cross-pollination is why a fairness system can suddenly get fast when someone brings a sum-check to it.