zkbox — Zero-Knowledge Certificates for Guardrail Heads

Prototype (Level A) of zero-knowledge proofs that a guardrail classifier's linear head certifies a convex harmful region — without revealing the head weights — implementing the certificates of Beyond Red-Teaming: Formal Guarantees of LLM Guardrail Classifiers (arXiv:2605.10901): the deterministic hyper-rectangle SAT/UNSAT certificate (Eq. 1 / Appendix B) and the probabilistic GMM coverage certificate (Eq. 2–3).

Stack: gnark v0.15.0, Groth16, BN254.

Box certificate (SAT/UNSAT, one circuit)

For a head $\mathrm{score}(x) = w'^{\top}x + b$ (weights already SVD-rotated into the box frame, publicly, outside the circuit), threshold $t = \ln\frac{\tau}{1-\tau}$, and an axis-aligned box $[l, u]$, one circuit proves either verdict, selected by a public mode bit:

$$\textbf{mode 0 (UNSAT — region fully flagged):}\quad \mathrm{PoK}\Bigl\{(\hat w, \hat b, r, \hat l, \hat u)\;:\; c_M \wedge c_R \wedge \sum_{i} \min(\hat w_i \hat l_i,\, \hat w_i \hat u_i) + \hat b - \hat t \ge \delta \Bigr\}$$ $$\textbf{mode 1 (SAT — verifiable safety hole):}\quad \mathrm{PoK}\Bigl\{(\hat w, \hat b, r, \hat l, \hat u, s)\;:\; c_M \wedge c_R \wedge x^{*} = \mathrm{corner}(s;\, \hat l + 1,\, \hat u - 1) \wedge \hat t - (\hat w^{\top}x^{*} + \hat b) \ge \delta \Bigr\}$$

with $c_M = \mathrm{Pedersen}(\hat w, \hat b, r)$ (head) and $c_R = \mathrm{Pedersen}(\hat l, \hat u)$ (region). Mode 0's sum is the closed-form minimum over the box (sign-selected corner, paper Eq. 1): every point of the region is flagged. Mode 1 exhibits a corner of the one-quantum-inward box — a point of the real region — scoring strictly below threshold: a publicly verifiable safety hole that reveals nothing about the head beyond the committed identity. One circuit means one trusted setup, so SAT and UNSAT proofs are linkable to the same $c_M$/$c_R$, and a pair of proofs at two thresholds brackets the region's minimum score. Both claims are mutually exclusive for the same statement by construction.

Boundary semantics: proofs exist only when the float margin $\lvert \mathrm{score}_{\min} - t \rvert$ clears the quantization band ($\approx 2\delta\cdot 2^{-64} \approx 10^{-5}$ in score units at BERT scale); inside the band neither claim is provable — inherent to sound fixed-point bridging, and the exporter refuses to emit statements there.

GMM / ellipsoid certificates (separate circuit family)

GmmCircuit proves the paper's probabilistic certificate for a committed RAW head and a committed GMM component set, $K$ components per proof (conjunction). Per component $c$, with $m_c = \hat w^{\top}\hat\mu_c + \hat b - \hat t$ and $\hat q_c = \hat w^{\top}\hat\Sigma_c\hat w$:

$$\textbf{mode 0:}\quad m_c \ge \kappa^{\mathrm{eff}}_c \cdot s_c + \delta_c \qquad\qquad \textbf{mode 1:}\quad \kappa^{\mathrm{eff}}_c \cdot s_c - m_c \ge \delta_c$$ $$\kappa^{\mathrm{eff}}_c = (1-2g_c)\,\hat\kappa_c,\qquad s_c^2 \;\ge\; \hat q_c + \mathrm{ridge}\cdot\lVert\hat w\rVert^2 \;\text{ (upper bracket, iff } \mathrm{mode} \oplus g_c = 0\text{)},\qquad s_c^2 \;\le\; \hat q_c - \mathrm{ridge}\cdot\lVert\hat w\rVert^2 \;\text{ (lower bracket, otherwise)}$$

The claim is parameterized by the public signed integer $\hat\kappa_c$ (scale $2^{16}$; the statement JSON carries signed strings, split in-circuit into a magnitude and a public sign bit $g_c$): mode 0 certifies $P_c \ge \Phi\bigl((1-2g_c)\hat\kappa_c/2^{16}\bigr)$ per component, mode 1 the upper bound — the sign bits unlock claims about levels below $\tfrac12$, which real checkpoints need. The aggregate coverage $\sum_c \pi_c,\Phi\bigl(\pm\hat\kappa_c/2^{16}\bigr)$ is computed OFFLINE by the verifier from the public record — no $\Phi$ in-circuit (gmm-verify prints it with directed guards). The sqrt-bracket side, the ridge sign ($\lceil d/2\rceil$ full / $1$ diag), and the variance-floor $\delta$-term all follow one invariant: upper bracket $\iff \mathrm{mode} \oplus g = 0$. The bracket always binds the side the prover would profit from; $\hat\kappa$'s magnitude is range-checked in-circuit and $g$ is asserted boolean (a rogue public $\hat\kappa$ or $g$ accepted by a sloppy verifier would flip the margin term — same failure class as the mode-boolean assert).

The GMM head is the RAW $w$ (verify_gmm.py does not rotate), so GMM-family $c_M$ has a different preimage AND a different setup than the box family's rotated $w'$ — the two families are unlinkable until a CP-link (Level B); vk_sha256 pinning plus the family field keep their artifacts apart.

Constant-time verification

$c_M$ and $c_R$ (or $c_G$ for the GMM family) are public statement constants, but not Groth16 public inputs: they are Pedersen commitment points carried inside the proof (gnark's frontend.Committer / BSB22, eprint 2022/1072) and compared by 32-byte point equality outside the constraint system. The only user-supplied public inputs are $\hat t, \delta, \mathrm{mode}$ (box) or $\hat t, \mathrm{mode}, \hat\kappa_{1..K}, \delta_{1..K}, g_{1..K}$ (GMM), so groth16.Verify is constant-time in $d$ (a v1 of this repo passed $\hat l, \hat u$ as $2d$ public inputs and paid an $O(d)$ MSM — see git history).

• Hiding of $c_M$: the committed $r$ is uniform in $\mathbb{F}_r$. Two gnark subtleties are handled and regression-tested: gnark's per-proof commitment mask is pinned to zero so the points are deterministic and publishable (commitment.ProverOpts — safe ONLY because $c_M$ carries its own randomness $r$ and the region/component preimages are public; never reuse the pattern for a secret-preimage commitment), and $r$'s wire is anchored in a constraint because a committed wire with no constraints gets a zero Pedersen basis and would silently drop out of $c_M$.
• Binding: DLOG over the SRS bases — the same honest-setup assumption as Groth16 soundness itself.
• Setup-relative: the points live in each circuit's trusted setup; publishing them pins (circuit, keys). A portable, cross-circuit commitment (LegoSNARK-style CP link) is the intended Level-B upgrade.
• gnark's Solidity exporter does not support multi-commitment proofs; on-chain verification (out of scope anyway) would need that gap closed.

Trust model — who checks what

Artifacts. vk_v3_d*.bin + ck_v3_d*.bin (box) and {vk,ck}_gmm{K}{cov}_v4_d*.bin (GMM) form one trust unit per family: the ck (commitment basis) is exported by setup because the verifying key alone cannot recompute Pedersen digests; both are public honest-setup CRS material and must reach the verifier through the same channel. Never accept a ck basis supplied by a region/record publisher — a fake basis inside the span of the true one makes an arbitrary record match an arbitrary digest.

Onboarding (amortized, once per region/record). The region record (region.json: quantized + exact float bounds; the rotation matrix $R$ is a sidecar identified by hash) is public. zkbox onboard-region validates the cleartext — $\lvert\hat l_i\rvert, \lvert\hat u_i\rvert < 2^{48}$, $\hat l_i \le \hat u_i$, $\hat l = \lfloor l\cdot 2^{32}\rfloor$, $\hat u = \lceil u\cdot 2^{32}\rceil$ — and recomputes $c_R$ over the trusted ck, publishing bound_w, bound_w_sat and the sat_capable flag (float provenance validated AND every $\hat u - \hat l \ge 2$ — exactly the condition for the open real interval to contain a grid point; thinner coordinates would let mode-1 corners escape the real box, a false-hole hazard). The GMM analog gmm-onboard re-derives $\hat\mu/\hat\Sigma$ from the float sidecars by round-half-even (the derivation IS the provenance), checks caps and $\sum\pi_c = 1$, and publishes per-component bound_mu, sigma_cap. Pedersen binding then transports these checks onto the in-circuit values in every proof. The circuits do NOT range-check committed region/component values (TestWrappingRegionSolvesInCircuit documents that an out-of-range region satisfies the constraints): a digest accepted without onboarding certifies nothing.

Per-proof verification ($O(1)$ box / $O(K)$ GMM). zkbox verify and gmm-verify refuse raw records and take the locally produced onboarded artifact. Checks: schema versions, $d$/$f$/family consistency, vk-hash pinning of both commitment files, $\mathrm{mode} \in {0,1}$, $\lvert\hat t\rvert < 2^{80}$, $1 \le \delta < 2^{96}$, the mode/sign-aware drift bound (below), commitment point equality, then the pairing check. The mode and sign bits are additionally asserted boolean IN-CIRCUIT, so non-boolean public bits admit no accepting proof at all.

Out-of-band anchor. That $c_M$ commits the deployed model's honest quantization is established when the owner publishes/attests $c_M$ — the proof links region ↔ committed head, not committed head ↔ deployment.

Quantization (fixed-point contract)

quantity	scale	rounding	enforced
$\hat w_i$	$2^{32}$	nearest	in-circuit: $\hat w_i \in [-2^{40}, 2^{40})$ (41-bit decomposition, MSB = sign)
$\hat l_i$	$2^{32}$	floor	at onboarding (transported by $c_R$)
$\hat u_i$	$2^{32}$	ceil	at onboarding (transported by $c_R$)
$\hat\mu_{c,i},\ \hat\Sigma_{c,ij}$	$2^{32}$	half-even	at onboarding: magnitude $< 2^{50}$ (transported by $c_G$)
$\hat b$	$2^{64}$	nearest	in-circuit: $\hat b \in [-2^{80}, 2^{80})$ (soundness-critical)
$\hat t$	$2^{64}$	ceil	per-proof validation
$\hat\kappa_c$	$2^{16}$	directed by mode/sign	in-circuit 20-bit magnitude check
$s_c$	$2^{48}$	ceil/floor isqrt per bracket	in-circuit 78-bit check
$\delta$	$2^{64}$	—	per-proof: $\delta \ge$ drift bound

Box drift bound: $\delta \ge \mathrm{bound_w}^{(\mathrm{mode})} + \lceil \lvert\hat t\rvert\cdot 2^{-50}\rceil + 2$, where the region part is published at onboarding (outward box for mode 0, inward for mode 1). GMM drift bound per component:

$$\delta_c \;\ge\; \mathrm{bound\_mu}_c + \mathrm{MuRoundCap}(d) + \Bigl\lceil \tfrac{\hat\kappa_c \cdot \mathrm{sigma\_cap}_c}{2} \Bigr\rceil + \underbrace{\hat\kappa_c \cdot \lceil 2^{48}/10^{6}\rceil}_{\text{iff mode} \,\oplus\, g_c = 0} + \bigl\lceil \lvert\hat t\rvert\cdot 2^{-50} \bigr\rceil + 2$$

Outward box rounding makes the quantized box a superset of the real box (inward for SAT claims, so exhibited corners are real points); the ridge $\lceil d/2\rceil\cdot\lVert\hat w\rVert^2$ dominates $\hat\Sigma$'s rounding as a quadratic form in the sound direction per bracket. A verified proof therefore implies the real-valued certificate for any float head whose honest quantization opens $c_M$ — including the oracle's $\sqrt{\max(\mathrm{var}, 10^{-12})}$ floor. No wrap: all box intermediates $< 2^{101}$, GMM intermediates $< 2^{155}$, both $\ll p/2 \approx 2^{253}$ (circuit/params.go, circuit/gmm_params.go). The plaintext certifier classifies the boundary $\mathrm{score}_{\min} = t$ as SAT; $\delta \ge 1$ keeps it unprovable, so ZK and cleartext agree there too.

Real-model results

All heads and datasets from the paper's artifacts; the cleartext oracles are the paper's actual Verifier.verify / verify_gmm.verify_gmm run on the same exported points.

Box (BERT urbas/bert_aegis, 10,000 construction points)

Both proofs are against the SAME published $c_M$ and onboarded $c_R$ — one setup, one committed head, one region:

statement	cleartext verdict	ZK outcome
$\tau^* = 0.5254$ (checkpoint's own), $t = 0.102$	SAT ($\mathrm{score}_{\min} = -6.415$)	mode-1 proof: verifiable safety hole, 228 B, verifies in 2 ms ✓
$\tau = 0.0009$, $t = -7.012$	UNSAT (margin 0.597)	mode-0 proof, 228 B, verifies in 2 ms ✓

The first row is the paper's Table 1 verdict (single hyper-rectangle on BERT is SAT at the operating threshold) as a zero-knowledge certificate. The proof pair brackets the region's minimum score between the two thresholds. A false UNSAT claim at $\tau^*$ fails at witness solving; a mode-flipped statement is rejected at validation (and by Groth16 public-input binding as the cryptographic backstop).

GMM coverage brackets (all three paper architectures)

model	config	oracle	ZK bracket (two 228-B proofs, same $c_M$/$c_G$)
BERT	$K{=}1$ full, paper $\tau^*{=}0.4773$	0.643666	$0.643607 \le P \le 0.643721$
BERT	$K{=}1$ full, own $\tau^*{=}0.5254$ ($P < \tfrac12$: sign bit)	0.190996	$0.190953 \le P \le 0.191040$
BERT	$K{=}1$ full, $\tau_{\mathrm{pess}}{=}0.1259$, mode 0	1.000000	$P \ge 1.000000$ ($\hat\kappa$ at cap) — Table-1 $\tau_{\mathrm{pess}}$ row
GPT-2	$K{=}3$ full, $\tau{=}0.37$ (comp. 2 at $\approx 0.2131$ via $\hat\kappa < 0$)	0.790942	$0.790938 \le P \le 0.790945$
Llama-3.1-8B	$K{=}3$ diag, $\tau^*{=}0.8003$ (comp. 0 at $\approx 0.0917$)	0.736190	$0.736185 \le P \le 0.736194$

Llama embeddings: 10,000 prompts extracted fp16 on MPS, ~67 min one-time, then 0.2 s per proof. An inflated-$\hat\kappa$ claim is rejected at $\delta$-validation, and with a compensating $\delta$ it fails at witness solving.

Benchmarks (Apple M4 Max)

Box circuit (./zkbox bench, bench.csv; constraints $\approx 47d + 190$):

d	constraints	setup	prove	onboard (once/region)	verify (per proof)	proof
16	946	42 ms	4 ms	0.4 ms	2 ms	228 B
64	3,202	104 ms	7 ms	1 ms	2 ms	228 B
256	12,226	345 ms	19 ms	2 ms	2 ms	228 B
768 (BERT/GPT-2)	36,292	0.9 s	55 ms	7 ms	2 ms	228 B
4096 (Llama-3.1-8B)	192,719	4.6 s	165 ms	37 ms	2 ms	228 B

GMM circuit (./zkbox gmm-bench, bench_gmm.csv; full covariance costs $(K{+}1)\cdot d(d{+}1)/2$ multiplications with pair products shared across components; diagonal is linear in $d$):

d	K	cov	constraints	setup	prove	verify	proof
768	1	full	625,066	22 s	1.2 s	2 ms	228 B
768	3	full	1,219,914	53 s	2.4 s	2 ms	228 B
4096	3	diag	201,996	5.4 s	0.2 s	2 ms	228 B

Verification is flat in $d$ for both families — the $O(d)$ (or $O(Kd^2)$) work moved into the once-per-region onboarding step.

Multi-box note

The paper's deterministic certifier loops over multiple hyper-rectangles (HDBSCAN clusters) and reports SAT if any box has a hole. This prototype proves one box per proof; a multi-box UNSAT certificate is $K$ proofs against the same $c_M$ (same keys, $K$ onboarded regions — all sharing one SVD frame). A shared-commitment multi-box circuit would follow the same K-block pattern as GmmCircuit.

Usage

go build -o zkbox ./cmd/zkbox

# ---- box certificate ----
./zkbox setup -d 768 -keys keys/                        # one-time per d; writes ck too
.venv/bin/python scripts/export_head.py \
    --model urbas/bert_aegis --dataset entfane/construction_points \
    --out-dir export/bert --embeddings-cache export/embeddings_bert.npy
    # --mode auto (default) emits the claim matching the cleartext verdict
./zkbox commit         -secret export/bert/secret.json -keys keys/ -out export/bert/commitment.json
./zkbox commit-region  -region export/bert/region.json -keys keys/
./zkbox onboard-region -region export/bert/region.json -keys keys/ -out export/bert/region_onboarded.json
./zkbox prove  -secret export/bert/secret.json -region export/bert/region.json \
               -statement export/bert/statement.json -keys keys/ -out export/bert/proof.bin
./zkbox verify -statement export/bert/statement.json \
               -region-onboarded export/bert/region_onboarded.json \
               -commitment export/bert/commitment.json -proof export/bert/proof.bin -keys keys/

# ---- GMM certificate ----
./zkbox gmm-setup -d 768 -k 1 -cov full -keys keys/
.venv/bin/python scripts/export_gmm.py --k 1 --cov full --threshold 0.4773 \
    --embeddings-cache export/embeddings_bert.npy --out-dir export/gmm_bert
    # emits statements for BOTH modes when provable (two-sided bracket)
./zkbox gmm-commit -d 768 -k 1 -cov full -secret export/gmm_bert/gmm_secret.json \
    -keys keys/ -out export/gmm_bert/gmm_commitment.json
./zkbox gmm-commit-record -record export/gmm_bert/gmm_record.json -keys keys/
./zkbox gmm-onboard -record export/gmm_bert/gmm_record.json -keys keys/ -out export/gmm_bert/gmm_onboarded.json
./zkbox gmm-prove  -secret export/gmm_bert/gmm_secret.json -record export/gmm_bert/gmm_record.json \
    -statement export/gmm_bert/gmm_statement_mode0.json -keys keys/ -out export/gmm_bert/proof0.bin
./zkbox gmm-verify -statement export/gmm_bert/gmm_statement_mode0.json \
    -record-onboarded export/gmm_bert/gmm_onboarded.json \
    -commitment export/gmm_bert/gmm_commitment.json -proof export/gmm_bert/proof0.bin -keys keys/

# benchmarks
./zkbox bench     -dims 16,64,256,768,4096 -out bench.csv
./zkbox gmm-bench -configs "768:1:full,768:3:full,4096:3:diag" -out bench_gmm.csv

secret.json / gmm_secret.json contain the head weights — never publish them. Everything else (records, statements, commitments, proofs, vk, ck) is public.

Versioning: JSON schema version 3 (loaders reject anything else). Key files carry the circuit revision in their names — box _v3_, GMM _v4_ (sign-bit circuit); commitments and onboarded artifacts are pinned to their setup via vk_sha256. Older artifacts are invalid: new circuit ⇒ new setup ⇒ new commitment values.

Layout

• circuit/ — BoxCircuit + GmmCircuit (two in-proof commitments each), fixed-point parameters and drift bounds (params.go, gmm_params.go)
• commitment/ — point extraction, native MSMs ($c_M$, $c_R$, $c_G$), commitment-key (ck) serialization, deterministic-commitment prover opts
• witness/ — v3 JSON interchange (decimal strings — $2^{64}$-scale values overflow JSON numbers; signed $\hat\kappa$ splitting), onboarding and per-proof validation
• prover/ — compile/setup/prove/verify wrappers, key & proof persistence, vk hashing
• internal/synth/ — synthetic provable instances for tests and benches
• cmd/zkbox/ — CLI (box: setup/commit/commit-region/onboard-region/prove/ verify/bench; GMM: gmm-* equivalents)
• scripts/export_head.py, scripts/export_gmm.py — exporters; both run the actual BRT certifier as the cleartext oracle and refuse to emit claims the oracle rejects (export_gmm.py --selftest checks the $\hat\kappa$-selection logic standalone)

Out of scope (future work)

Portable CP-SNARK commitment linking across circuit families and to a canonical head commitment (Level B composition; design note tracked outside the repo), transformer-body proofs, shared-commitment multi-box circuit, in-circuit $\Phi$ for secret coverage levels, on-chain verification.