VEIL: Lightweight Zero-Knowledge for Hash-Based Multilinear Proof Systems

Formal Verification Audit Document

Rahul Dalal, Tamir Hemo, Eugene Rabinovich, Ron D. Rothblum — Succinct

The security properties of the VEIL protocol have been formally verified in Lean 4. Specifically, the axioms, definitions, and theorem statements from the paper have been encoded in Lean, and the proofs have been machine-checked. The formalization was produced primarily by AI (Claude Opus 4.6 and 4.7) under human supervision. However, there is no formal guarantee that the Lean statements faithfully match the VEIL paper or any implementation—this correspondence must be audited by humans.

This document is designed to make auditing correspondence with the paper as easy as possible. It presents all major definitions and theorems alongside their Lean formalizations. Click any Lean link to view the formal statement side-by-side. Within the Lean code, hoverable identifiers show the definitions they depend on.

To verify the proofs, clone the source repository and run lake exe cache get && lake build to compile and type-check all theorems and also verify that no spurious axioms were added. For independent kernel-level validation, run lake env leanchecker afterward. See the Lean reference on validating proofs for standard guidelines (note: some instructions on that page may be outdated).

Card Types

Definition

Formal definitions from the paper

Theorem

Main security properties proved

Axiom Class

Axiomatized cryptographic assumptions

1. Preliminaries

DefinitionRelative Hamming Distance (§2)

1.1 Error-Correcting Codes

DefinitionLinear Code (§2.1)

Axiom ClassMinimum Distance (§2.1)

Zero-Knowledge Codes

Axiom ClassZK Code (Definition 2.1)

Multiplicative Codes

DefinitionHadamard Product (Definition 2.3)

Axiom ClassMultiplicative Code (Definition 2.4)

Axiom ClassReduction Function (Definition 2.8)

1.3 Proximity Gaps

DefinitionInterleaved Distance (§2)

Axiom ClassProximity Generator (Definition 2.14)

Axiom ClassLinear Bias Generator (Definition 2.16)

1.2 Multilinear Polynomials

DefinitionEquality Polynomial (§2.3.1)

DefinitionMultilinear Evaluation (§2.3.1)

2. How to Read Protocol Sections

Each protocol section below is split into definitions (green boxes) followed by theorems (blue boxes).

Definitions

Every protocol is defined in LEAN using the same core objects. Together they should fully specify what the protocol does:

Parameters— the cryptographic setup: codes, distances, proximity generators, query counts.
Verifier View — a single struct bundling everything the verifier sees: public input, verifier randomness, and transcript (prover messages + oracle query responses). Both realView and cheatingView produce a VerifierView, and verifierAccepts takes only a VerifierView.
Real View — how an honest execution populates the VerifierView. Defines the protocol flow: commitment phase (padding, oracle construction), interaction phase (prover/verifier messages), and query phase.
Verifier Acceptance — the predicate the verifier checks, taking only a VerifierView. Lists the algebraic checks the verifier performs on the transcript.
Cheating View — how an adversarial execution populates the VerifierView. A CheatingProver is a collection of response functions, each producing one part of the transcript. The function arguments encode the round structure: they show exactly which verifier challenges the cheating prover has seen when generating each response. For example, a field respond : F → Vec F n means the prover's response may depend on one challenge, while a constant field β : F means it is fixed before any challenge is seen. The oracle is committed upfront and is immutable — query responses are lookups into this fixed table.

Theorems

Each protocol proves three properties, stated in terms of the definitions above:

Completeness — verifierAccepts(realView(...)) always holds when the claim is true.
Binding (Soundness) — for any oracle, there exists a bound witness such that verifierAccepts(cheatingView(...)) holds with low probability when the claim is false.
Zero-Knowledge — there exists a simulator such that for any value of verifier randomness, its output distribution equals the distribution of realView(...) over the prover's randomness.

Global Variables

3. Commit-and-Prove Protocols

3.1 ZK Lin-Eval PCS — Lemma 3.4 (zk-dot-product)

Protocol Definition

Parameters(Lemma 3.4)

DefinitionPublic Input (Figure 2)

DefinitionVerifier View (Figure 2)

DefinitionReal View (Figures 1–2)

DefinitionVerifier Acceptance (Figure 2)

DefinitionCheating View (Figure 2)

Theorems

TheoremCompleteness (Lemma 3.4)

TheoremBinding (Lemma 3.4)

TheoremZero-Knowledge (Lemma 3.4)

3.2 ZK Hadamard-Eval PCS — Lemma 3.6 (zk-hadamard)

Protocol Definition

Parameters(Lemma 3.6)

DefinitionPublic Input (Figure 4)

DefinitionProver Input (Figure 3)

DefinitionVerifier View (Figure 4)

DefinitionReal View (Figures 3–4)

DefinitionVerifier Acceptance (Figure 4)

DefinitionCheating View (Figure 4)

Theorems

TheoremCompleteness (Lemma 3.6)

TheoremBinding (Lemma 3.6)

TheoremZero-Knowledge (Lemma 3.6)

3.3 ZK Circuit Evaluation — Lemma 3.9 (zk-R1CS-eval)

Protocol Definition

Parameters(Lemma 3.9)

DefinitionPublic Input (Figure 6)

DefinitionVerifier View (Figure 6)

DefinitionReal View (Figures 5–6)

DefinitionVerifier Acceptance (Figure 6)

DefinitionCheating View (Figure 6)

Theorems

TheoremCompleteness (Lemma 3.9)

TheoremBinding (Lemma 3.9)

TheoremZero-Knowledge (Lemma 3.9)

4. Compiling into a ZK IOP

4.1 Intermediate Compilation — Lemma 4.3

Compiles an arithmetically partially-zk IOP into a fully-zk IOP by hiding exposed messages with a random masking vector and delegating acceptance to a circuit evaluation scheme.

Abstract Sub-Protocols

DefinitionBase Protocol Params (Definitions 4.1 & 4.2)

DefinitionBase Protocol (Definitions 4.1 & 4.2)

DefinitionCircuit Evaluation Scheme (Definition 3.1)

Compiled Protocol

Parameters(Lemma 4.3)

DefinitionCompiled View (Figure 7)

DefinitionCompiled Real View (Figure 7)

DefinitionCompiled Verifier Acceptance (Figure 7)

DefinitionCheating View (Figure 7)

Theorems

TheoremCompleteness (Lemma 4.3)

TheoremSoundness (Lemma 4.3)

TheoremZero-Knowledge (Lemma 4.3)

4.2 ZK Multilinear PCS — Lemma 4.7

Abstract Sub-Protocol

DefinitionFactored Oracle

DefinitionBase MCS (Definition 4.5)

Protocol Definition

Parameters(Lemma 4.7)

DefinitionPublic Input (Figure 9)

DefinitionVerifier View (Figure 9)

DefinitionVerifier View — Shielded Part

DefinitionReal View (Figure 9)

DefinitionVerifier Acceptance (Figure 9)

DefinitionCheating View (Figure 9)

Theorems

TheoremCompleteness (Lemma 4.7)

TheoremBinding (Lemma 4.7)

TheoremPartial Zero-Knowledge (Lemma 4.7)

4.3 Final Compilation — Lemma 4.8

Abstract Sub-Protocols

DefinitionBase MIOP Params (Lemma 4.8)

DefinitionBase MIOP (Lemma 4.8)

DefinitionMultilinear PCS (Lemma 4.7)

Compiled Protocol

Parameters(Lemma 4.8)

DefinitionCompiled Verifier View (Figure 10)

DefinitionCompiled Acceptance (Figure 10)

DefinitionCompiled Shielded View (Figure 10)

Theorems

TheoremCompleteness (Lemma 4.8)

TheoremSoundness (Lemma 4.8)

TheoremPartial Zero-Knowledge (Lemma 4.8)

Click a Lean link to view the formal statement here.