Three ideas, and the second and third both matter well beyond this paper. (1) CIRCUIT-EMBEDDED WEIGHTS. Because the model is public, the weights are compiled into the R1CS as CONSTANTS rather than passed in as signals. R1CS charges nothing for multiplication-by-constant, so every linear layer -- every matmul, every convolution, and BatchNorm folded into it -- costs LITERALLY ZERO CONSTRAINTS. Proving cost is then a function of one thing only: the number of non-linearity calls. This is the same conclusion the sum-check line reaches (matmuls are nearly free; the money is at the non-linear seams) arrived at from a completely different direction, and it is worth having both. Measured effect (Table 5): ResNet18 drops from 37.85M constraints to 1.16M (~32x) and from 270 s to 14 s. The catch is that it is only available because the weights are public -- this optimization is structurally unavailable to every MLaaS system in this table. (2) ULTRAGROTH. Lookup arguments inside Groth16, which is supposed to be impossible: LogUp (Haboeck) needs a verifier challenge sampled AFTER the witness is committed, and Groth16 has no rounds. UltraGroth adds them -- the witness is split into d+1 "rounds", each round's commitment is hashed to derive the next round's challenge (Fiat-Shamir with an in-circuit random oracle), and the extra commitments ride along in the proof. Cost: one extra pairing (4 instead of 3), one extra hash, and d+1 extra G1 elements. Proven complete, sound and zero-knowledge in GGM+ROM (Appendix A). This is the interesting cryptographic contribution and it is buried in a vendor tech report. The payoff: a ReLU's range check drops from b constraints to b/w, with w the limb size; prover complexity O(2^(w+1) + bL/w + 4L) for L range checks, i.e. O(N / log N). (3) THE RESCALE SEAM IS FREE, WHEN IT RIDES ON A ReLU. This is the fact the numerics page should carry. ReLU already bit-decomposes its input to determine the sign -- that IS the range check. Once you have the bits, dropping the low l*rho of them is a right shift that costs NOTHING: "Computing ReLU(x) >> rhol for some fixed l costs b+1 constraints" -- the same b+1 as a bare ReLU. The rescale after a matmul, which every other system in this corpus pays for at every seam, is here fused into a decomposition it was already buying. It is the strongest form of the "round less often / fuse the seam" result that zkGPT (constraint fusion), DeepProve (delayed requantization) and Jolt Atlas (i64 rebase) each found independently -- and Bionetta found it a fourth time, citing none of them for it. AND THE COROLLARY IT DRAWS, WHICH CONTRADICTS SAFETYNETS. Bionetta explicitly rejects polynomial activations (pi-nets), and its reason is the seam: a degree-d polynomial costs only d constraints per value, but it RAISES the precision of the result by rhod bits, which forces a precision cut, which costs ~b constraints. "The benefit of d constraints per value is lost in the overhead of precision cuts." Read that against SafetyNets, whose whole cost advantage comes from quadratic activations having no rescale seam at all: Bionetta is saying the seam does not disappear under a polynomial activation, it just moves to where the precision blew up. Nobody has reconciled these two claims and they are both in this corpus. WHAT IT CANNOT DO. No softmax, no attention, no LayerNorm, no transformer, no general ONNX. The supported non-linearities are exactly ReLU, LeakyReLU (alpha a power of two only), ReLU6, HardSigmoid and HardSwish -- the ReLU family, chosen because they are the ones whose cost the sign-bit decomposition already pays for. ActivationOps.from_keras in the SDK maps Softmax to NOT_SUPPORTED. Do NOT put this system on the tokens-per-minute axis; it is not an LLM prover and does not claim to be.

INVERTED relative to every other system in this category, and this is the single most important fact about the paper. The rest of the verifiability column is MLaaS: the SERVER proves, the WEIGHTS are the secret, and the client is the verifier. Bionetta is the opposite -- the CLIENT proves, on their own phone, over a PRIVATE INPUT, against a model whose weights and architecture are PUBLIC. Its motivating applications are biometric proximity ("this face matches the enrolled template") and liveness, where the thing worth hiding is the user's face, not the network. The library's own README states the limit in a warning box -- "the library is not intended for private model weights + public input proving. The library is designed only for public model weights + private/public input proving!" -- which is a restriction the paper's abstract does not mention. Every claim it makes should be read inside that box. It is not competing with DeepProve or zkGPT; it is answering a different question, and it is the only system in this corpus that does.

Read the threat model before you read anything else, because every number in this paper is downstream of it and the abstract does not tell you.

Every other system in proving inference is MLaaS: a server holds a valuable model, runs it on your input, and proves it did so honestly. The weights are the secret. The server is the prover. Bionetta is the exact inverse, the model is public, the input is private, and the client is the prover, on their phone. The motivating application is a biometric one: prove that your face matches an enrolled template, without handing anybody your face.

The library's own README says the limit out loud, in a warning box, which the paper never does:

Despite astounding performance, the library is not intended for private model weights + public input proving. The library is designed only for public model weights + private/public input proving!

Bionetta README (Anonymous1725/Bionetta) · About

So it is not competing with DeepProve or zkGPT, whatever the benchmark tables suggest. It is answering a question nobody else in this corpus answers, and it is the only entry here whose prover is a phone.

What is new

Circuit-embedded weights, and it is almost embarrassingly simple. R1CS charges nothing for multiplication by a constant. If the weights are public, they do not have to be signals, they can be compiled into the constraint system as constants. So every linear layer, every convolution, and every BatchNorm folded into one, costs exactly zero constraints. Not "cheap". Zero. Proving cost then depends on one quantity: the number of non-linearity calls.

The effect is the largest single lever in the paper: ResNet18 falls from 37.85M constraints to 1.16M, and from 270 seconds to 14. And it is structurally unavailable to every MLaaS system in this SoK, because theirs is the case where the weights are the thing you are hiding. This is the clearest demonstration in the corpus that the threat model, not the proof system, is the dominant term in the cost.

It also lands on the same conclusion the sum-check line reached from the opposite direction. GKR says: matmuls are nearly free, so the money is in the non-linear seams. R1CS-with-constant-weights says: matmuls are literally free, so the money is in the non-linear seams. Two entirely different proof systems, one cost model. That agreement is worth more than either paper's benchmark.

UltraGroth is the cryptographic contribution, and it is the thing that should not be buried in a vendor tech report. Lookup arguments need a verifier challenge sampled after the witness is committed, LogUp's rational-sum identity is checked at a random point, and the prover must not know the point in advance. Groth16 has no rounds, which is exactly why nobody puts lookups in it.

UltraGroth adds rounds. The witness is split into $d+1$ segments; each segment gets its own $\delta_i$ and its own commitment $\pi_C^{\langle i \rangle}$; the commitment is hashed to derive the next segment's challenge, and the challenges are carried as public signals the verifier recomputes. The proof grows to $\pi_A, \pi_B, \pi_C^{\langle 0 \rangle} \dots \pi_C^{\langle d \rangle}$, and verification goes from three pairings to four. That is the entire price: one pairing and one hash buys lookup arguments inside Groth16. Completeness, soundness and zero-knowledge are proved in GGM + ROM in Appendix A.

What it buys downstream is the range check, which, per the numerics page, is where the whole proof actually lives. A ReLU's $b$-constraint bit decomposition becomes $b/w$ lookups for limb size $w$, giving prover complexity $O(2^{w+1} + bL/w + 4L)$ over $L$ range checks, i.e. $O(N/\log N)$. The paper solves for the optimal $w$ ($2^w w^2 = Lb / 2\log 2$, landing near 18); the shipped SDK defaults to 15.

The rescale seam is free. This is the fact that changes how the numerics page has to be written, and Bionetta states it in one line and moves on.

ReLU already decomposes its input into bits, that is how you get a sign out of a field that has no order. But once you have the bits, a right shift is free: you simply drop the low ones. So the precision cut, the rescale, the thing every other system in this corpus pays for at every seam, costs nothing extra when it rides on a ReLU it was already paying for. The paper's proposition is that ReLU(x) >> ρℓ costs $b+1$ constraints, which is the same $b+1$ as a bare ReLU.

Everyone else fuses seams to make them cheaper: zkGPT's constraint fusion, DeepProve's delayed requantization, Jolt Atlas's i64 accumulate-and-rebase. Bionetta fuses the seam into an operation whose cost it had already spent, which makes it not cheaper but free. It is the strongest form of the result, it is the fourth independent discovery of it, and it cites none of the other three for it.

What it actually proves

One forward pass of a convolutional or fully-connected network, in fixed point with $\rho$ fractional bits, over a public model, on a private input, under a per-circuit Groth16 trusted setup.

Every clause there is load-bearing:

• One forward pass. No tokens, no sequence, no autoregression. claim_kind: pass.
• CNNs and MLPs only. The supported non-linearities are ReLU, LeakyReLU (with $\alpha$ a power of two, anything else is rejected), ReLU6, HardSigmoid and HardSwish. That is the ReLU family, and the selection is not arbitrary: those are precisely the activations whose cost the sign-bit decomposition already pays for. There is no softmax, the SDK's ActivationOps.from_keras maps tf.keras.layers.Softmax to NOT_SUPPORTED, and therefore no attention, no LayerNorm, no transformer. It is not on the tokens-per-minute axis and should never be put there.
• Per-circuit trusted setup, which cuts two ways and both are interesting. The cost: retraining the model means a new ceremony, which makes this unusable for anything that updates its weights. The benefit, which nobody states: a Groth16 verification key is a commitment to the exact circuit, and the circuit is the architecture. This is the strongest architecture-pinning in the corpus, stronger than zkAudit's public-architecture convention, and it means the precondition of the Fiat–Shamir/GKR attack (the prover chooses the circuit) is cryptographically out of reach here. Bionetta is one of the two systems in this SoK the attack cannot touch, and it got there for free, as a side effect of a design choice made for other reasons.

The benchmarks, and what they actually settle

Two results in Bionetta's Table 4 are more useful to this SoK than its own headline, and neither is about Bionetta.

The Halo2 story is wrong in the half nobody checks. Our own proof systems page says what everyone says: PLONKish is the slow-prover/fast-verifier bargain, and you tolerate the prover because kilobyte proofs and millisecond verification are what make on-chain settlement possible at all. Bionetta measured it. As ezkl actually ships, proofs are hundreds of kilobytes, verification keys reach tens of megabytes, and verification takes seconds to tens of seconds, 40.6 s on MobileNetV2, behind a proving key of 76 GB. None of that is going on a chain. Halo2 can be configured for small proofs; the toolchain people deploy is not, and until now nobody had published the numbers. Meanwhile ZKML, the other Halo2 system, on the same hardware and the same models, verifies in 12–23 ms with 5–7 kB proofs. The two most-deployed PLONKish zkML toolchains do not have the same verifier profile, and the literature treats them as one row.

zkCNN is still the fastest prover on small models, five years on. Bionetta beats it only above roughly 2M parameters, and loses to it below, zkCNN proves LeNet5 in 1.05 s against Bionetta's 3.75 s. What zkCNN pays is what GKR always pays: 23–43 kB proofs and verification in the hundreds of milliseconds to seconds. The 2021 trade has not moved. Only the models have.

What to distrust

The comparison is not the comparison it looks like. Bionetta's linear layers are free because its model is public. ezkl's, ZKML's and zkCNN's are not free because theirs are not. A great deal of the headline gap is therefore not a proof-system result at all, it is the threat model, showing up in the constraint count. The paper never separates the two, and a reader skimming Table 4 will attribute to UltraGroth a win that belongs to a weaker security setting. (To be fair to the paper: its own Table 5 does isolate the two effects, and it is the most honest table in the report. It just is not the one anybody will quote.)

The precision result is real, and it points somewhere the paper does not look. Bionetta measures relative error against TensorFlow at $\rho \in \{15, 30, 45, 60\}$ and gets $5.2\times10^{-3}$ down to $9.4\times10^{-7}$, four orders of magnitude of accuracy, while the constraint count does not change at all, because the bit decomposition is over the 254-bit field element either way. This is DeepProve's "four more bits costs under one percent" finding, reproduced in a completely different proof system, and neither paper knows about the other. See the open question it jointly sharpens. (The shipped SDK's default is $\rho = 15$, the least accurate setting the paper measured.)

The polynomial-activation argument contradicts SafetyNets, and nobody has noticed. Bionetta rejects polynomial activations for a specific reason: a degree-$d$ polynomial costs $d$ constraints per value, but raises the precision of the result by $\rho d$ bits, forcing a precision cut that costs $\approx b$. "The benefit of $d$ constraints per value is lost in the overhead of precision cuts." Now read SafetyNets, whose entire cost advantage, a few percent of overhead, three to six orders of magnitude better than anything since, comes from quadratic activations having no rescale seam at all. Both claims are in this SoK. They cannot both be the whole truth, and the reconciliation (SafetyNets is shallow, and precision growth is exponential in depth) is a paragraph nobody has written.