# Weight hiding

**In short.** Masking is on by default: by design, beyond a [declared list](../docs/what-is-not-hidden.md), every published value that depends on the weights is masked or published only as a salted hash. Zero knowledge, Lean's form of weight hiding, is proved in Lean for the protocol, at [full size](terms.md) and at the exact-match policy, with fresh random masks. The honest prover in these theorems is a Lean definition, not the CUDA prover. For the interactive protocol (IOP) it is honest-verifier zero knowledge. For the compiled (non-interactive) prover and the Lean verifier that is proved sound, in the random-oracle model, it holds against any verifier within 2^64 hash queries and 688,127 replies, on one [leaf table](terms.md): all that such a verifier sees can be simulated from the public files, the requests and one bit per request (served or refused: a request is refused if it is ill-formed, if the model has no result on it, or if its result is other tokens), up to a statistical distance below 2^-154. That bit is revealed, and it depends on the weights. A service that chooses to say "failed" (that is not the shipped programs' own "failed": [limits](../docs/limits.md#narrower-than-what-runs)) reveals one label of three in its place (served, failed or other tokens). The programs are tested, not verified: in honest runs (unchanged programs, no compiler or hardware fault) of [the released programs](../docs/limits.md#what-was-run-on-these-programs) we have seen nothing beyond the declared list, though no test on them hunts for a leak. With the protocol's conditions kept we know of no attack, though few were sought. Outside these conditions hidden values have come out in trials, not on the released programs (rows H1 and H46.4 of [the table](../docs/limits-all-rows.tsv)). That no other kind of leak has been found does not mean that there is none. So, for a research prototype, we expect, rather than know, that the programs hide the weights at the default setting, in honest runs, if the provider keeps its duties (this does not reach any real model's weights, or the parameter file and scales fitted to them; the conditions in full: [docs/limits.md](../docs/limits.md#the-verdicts-own-conditions)).

**What bounds that.** Lean's theorems are about a Lean definition of the prover, default values included, with fresh random masks: nothing is proved for the programs, which derive their masks from a secret seed. They are for one commitment and one request to a proof, and after compiling for one [leaf table](terms.md) and exact match: batches, which are what the programs serve, are not covered. Nothing in the Lean prover counts replies, and beyond 2^64 hash queries or 688,127 replies the compiled theorem says nothing. Neither do they say anything of what the public files themselves tell of the weights, or of timing. The independent checker has accepted the soundness theorem on `verify` (`sound_of_verify_at`), with every declaration beneath it, and nothing that does not lie beneath it, in a pass on that theorem's export alone: the exporter wrote that export out of a copy of the compiled files of this repository's build (that the compiled files it read were that build's is known from a report alone; Lean's own files were not compared with a list of checksums); the results on weight hiding stated here ([lean/LIMITS.md](../lean/LIMITS.md), L62 to L65, L91, and L93's line on zero knowledge) are not among what the checker accepted in that pass, and for them there is Lean's own kernel alone (the pinned version of Lean is older than published fixes of soundness bugs: [lean/LIMITS.md](../lean/LIMITS.md), L45; [lean/CHECK-RESULTS.md](../lean/CHECK-RESULTS.md); what such a pass is worth, and why a reader cannot repeat it: [lean/CHECKING.md](../lean/CHECKING.md), "The independent checker"). Little has looked for a leak or an attack. What was tested is the default setting, mostly on synthetic weights and at small size. A provider's own model needs a parameter file and scales fitted to it; only one of our five tests has run on a real model's weights. There has been no independent security audit. So try it on public or synthetic weights before you trust it with weights that you cannot afford to lose.

*Weight hiding* is the goal that clients and the public learn nothing about a model's weights beyond a [declared list](../docs/what-is-not-hidden.md) (not shown to be complete): among others each reply, the architecture, timing, failures, and scales chosen from the weights (how much these tell has not been worked out). By design, every other published value that depends on the weights is masked (a random value is added) or published only as a salted hash. Masking is on by default. The words used here: [Terms](terms.md).

## The protocol

The provider encodes its weights with random masks and publishes a commitment (a fingerprint of that encoding) with a public key file. A proof has three parts, each with its own prover: the key file's proof (the encoded weights are in range; made once), the link proof (a further encoding holds the same weights) and the request's proof (the reply is the model's). Proofs open columns of an encoding, whose masks cover a fixed budget of openings. The protocol's proximity tests (those analysed by mutual correlated agreement) work beyond half the minimum distance; that needs out-of-domain samples on the committed tables (masked sums of the weights, published with the commitment).

Zero knowledge means that all a verifier sees could be produced ("simulated") without the weights, from the public settings and each proof's prompt and output tokens. The settings include scales chosen from the weights, so zero knowledge says that the weights are hidden only among those that fit one configuration. What [Lean](../lean/THEOREM.md), a proof assistant, proves of it for the protocol:

| Part | What Lean has |
|---|---|
| Before hashing, the interactive protocol (IOP): the key file's proof, the link proof, a request's proof | proved, at full size: honest-verifier zero knowledge of the three honest provers, which are Lean definitions. Each run is simulated exactly, but where the prover stops for a private reason: the chance of that is 0, 0 and at most 2^-174. Over the whole life of one commitment, a budget that the statement fixes (up to 710,324 leaf tables with 688,127 requests each): within 2^-135 |
| After hashing (Fiat-Shamir), in the random-oracle model | proved: zero knowledge of the compiled committer and prover, with the Lean verifier that is proved sound, against any verifier within 2^64 hash queries and 688,127 replies, at a statistical distance below 2^-154; one commitment with one leaf table, one request per proof, exact match, fresh random masks |
| Revealed | one bit per request: served or refused; it depends on the weights (in a corollary, for a service that says "failed": one label per request: served, failed or other tokens) |
| Batches; a second commitment; timing; what the public files themselves tell of the weights | nothing |
| The C++ and CUDA programs | nothing: not proved; tested |

These numbers are statistical distances, not a security level. The simulators' running time is not modelled. The theorems assume that the verifier makes no hash query before the commitment, and that the weights and the public files are fixed before the hash function is drawn. A second, fixed hash function inside the format is not treated as random. The long form, with every bound: [docs/limits.md](../docs/limits.md#where-it-stands). Behind the programs' counter no Lean theorem stands: nothing in Lean keeps count of the columns that a table has opened. Whether the model [can serve](terms.md) a request depends on the weights and is visible; that a request to a real model is one that it can serve is not proved ([Known limits](known-limits.md)).

The protocol takes its building blocks from a published paper ([CFW26] in [our paper](../paper/paper.pdf)), where they are proved by hand; the protocol uses them with changes, so these proofs do not carry over by themselves. A written proof of hiding for the whole protocol, in a technical report of this project, is not public and not settled: checked too little to rely on, and nearly every time that a whole part was read, further sentences were found that were false as worded ([how it was checked](../docs/limits.md#on-paper)). Two points on the one lemma that it rests on are open, and further points are open between what Lean proves for the protocol, the written proof and the protocol as run ([by name](../docs/limits.md#where-it-stands)). With the protocol's conditions kept (each mask random, secret and used once; each encoding opened within its limit; secret seeds independent), we know of no counterexample or attack on the protocol; few were sought: only one step, the out-of-domain samples on the committed tables, has been attacked on purpose, on paper. A kept row's 219 random values for 219 shown positions, with no slack, are argued on paper only. What Lean proves is statistical, with the hash as a random oracle and for truly random masks; with the programs' seed (ChaCha20) hiding can be computational at best.

## The programs

They are written to follow the protocol. Five tests check that the masks are there and whether a lost mask is noticed; none hunts for a leak. We judge that weight hiding likely holds at the default setting, in honest runs, if the provider keeps its [duties](serving.md#the-providers-duties). The judgement is given of the released programs: the first and the fifth of its five tests have run on them, with the outcomes told under [five tests](../docs/limits.md#verdict-runs), both at small size on synthetic weights and the first at full size too, once on synthetic weights and once on a real model's public weights; the fifth ran once. The second and the third ran on test builds of [other sources](../docs/glossary.md#other-sources), and the fourth on programs of other sources; at full size the fifth's two audits ran together only on programs of other sources. The one whole reading of the sources was of a text from which these differ in code in 68 of 384 files, and in 136 more in comments, names and the wording of messages alone; two more of the 384 are not among these sources; in the 68 the differences in code were read for hiding, by difference alone, apart from renamed names and reworded messages, and the files were not read whole again (row HW-745 of [the table](../docs/limits-all-rows.tsv); [on which programs it was made](../docs/limits.md#on-which-programs)). That judgement rests on the design, what is proved in Lean for the protocol (above), code review (whole files, read once and fast, with nothing built or run: [the readings](../docs/limits.md#verdict-reading)) and tests; it is not a proof.

<a id="the-main-bad-results-in-tests"></a> **Not shown.** Only one of the five tests ran on a real model's weights, four times, of which once on the released programs (there all 4,096 sums that it checked were masked, which does not show that the masks hide), so the judgement does not cover them; no problem is known. Recovering weights from published files has barely been tried.

**Bad results.** A mask lost to a bug or hardware fault can leave an unmasked value in a file that verifies. Of 165 random values destroyed on purpose in CPU memory, 123 were stopped, 12 changed no file and 30 went unnoticed; all 130 in GPU memory were stopped, 122 of them by one self-check alone (picked cases on test builds of other sources, at small size, on synthetic weights: no rate).† In one trial†, with a BF16 weight file, somebody who could write that file but not read it learned the magnitudes of two neighbouring weights in about 32 starts ([more](../docs/limits.md#files-of-8-or-16-bits)). [The tests' outcomes](../docs/how-hiding-is-checked.md).

## If your weights must stay secret

- **What our judgement covers:** weight files that store no tensor in 8 or 16 bits, with the default setting's parameter file (the shape of Llama 4 Maverick, and small test forms; also with a clipped-gap policy's three numbers set in it, on less evidence: all five tests ran under exact match). The judgement takes in batches that overlap in time, as they do by default (every Lean result on hiding is for one request per proof, so none covers them; no attack is known, and only three short readings looked for one; no test was aimed at them), and batches with a failed request, which a client can cause (the other requests' files have not been examined), both on thin ground: ["The default's own overlap" and "Batches with a failed request"](../docs/limits.md#what-a-reader-cannot-repeat-on-hiding). Anything else is outside it, and so is any real model, the example's too, because it needs a parameter file fitted to it; the programs accept all of it without a warning.
- **The counter.** The secret key directory, the provider's own, holds the seed and a counter. The prover counts the batches that each encoding (a leaf table) serves and stops at a limit (688,127 at full size). A copied or restored directory has an older count; past the limit proofs give away exact equations in the weights, unnoticed. Never copy, back up or restore it. The number of that limit also appears in Lean's theorems, where it counts another thing (replies, each to one request; the counter counts batches of up to 64 requests), so the counter's limit is not the theorems' bound. A lost disk or a second GPU means a new commitment, which our judgement covers on thin ground and on [conditions of its own](../docs/limits.md#a-further-commitment) (Lean has no statement on hiding for more than one commitment): a count over two small commitments found no derived random value twice† (a check for gross faults only), and no test has searched two together for leaks.
- **The seed.** The public files hold masked sums of the weights for good, and whoever reads the seed can strip the masks. With `-public-weights` nothing is hidden.
- **Checks.** The prover does not verify its proofs. The vLLM integration that ships hands on no proof, and nothing of its response, before `cp_verify` has passed every proof of its batch (narrow exceptions, none open to a client: [integrations/LIMITS.md](../integrations/LIMITS.md#narrow-exceptions)); `driver/measure_rate.py` reports no rate, and an example script shows no answer, before `cp_verify` has accepted the proofs; and a front end of your own must do the like: after a bug or a hardware fault a response that `cp_verify` rejects can hold unmasked values ([more](../docs/limits.md#a-response-that-does-not-verify)). That check can miss a lost mask. The audit with the key, which recomputes part of the published bytes from the secrets, accepts only commitments to synthetic weights: on a real model's files you cannot run it.
- **Clipped gap,** the tolerant acceptance policy and the expected use: each outcome tells a client something about the model's scores; how much many outcomes tell together has not been bounded. Lean's theorem on zero knowledge is for exact match: under a clipped-gap policy no Lean theorem covers what a whole proof reveals, and all five tests ran under exact match. Beside the five, both audits with the provider's secrets ran under such a policy, at small size, on the released programs: they show that the masks are there as derived, which is no search for a leak (row H13.8 of [the table](../docs/limits-all-rows.tsv)).
- Breaking a duty can leak weights while every proof verifies; what a breach gives away has not been tried on the released programs ([all the duties](../docs/operators-duties.md); [further conditions](../docs/limits.md#further-conditions)).

† Not on the released programs: [which kinds of result these are](../docs/limits.md#on-other-programs).