Nullark has completed one bounded fund-safety result for the exact deposit and withdrawal artifacts selected by the current SDK. Completed claim. When the exact generated-verifier runtime accepts a deposit or withdrawal proof, Lean reaches one of two machine-checked outcomes:
  1. the proof yields a witness for the matching frozen constraints, and that witness refines to the fund-safety result; or
  2. the proof exposes an explicit setup-root break.
A setup-root break means a nonzero verifier polynomial evaluates to zero at the sampled setup point. The term names the theorem’s cryptographic failure branch; no incident is being reported. This result stays with those exact artifacts. A different artifact set needs the same binding and review.

​
How the completed claim closes

Runtime to Groth16 equation. Generated-verifier semantics and verifier-key binding show that a successful runtime call accepted the canonical BN254 pairing equation for this proof and public-input order. Groth16 acceptance to witness or break. The Type III knowledge-soundness path returns either a matching witness or concrete failure data. Type III names the two-group pairing setting used here. AGM, the algebraic group model, lets the theorem track how proof elements were built from setup elements. The failure data is a nonzero check polynomial that still evaluates to zero at the hidden setup sample. This is the setup-root break: acceptance occurred at the sampled point without the polynomial identity needed to extract a witness, so the fund-safety path ends there. Witness to fund safety. QAP is the polynomial form checked by Groth16; R1CS is the frozen list of circuit constraints. The exact QAP-to-R1CS certificate proves that both describe the same rules and public inputs. Semantic refinement then decodes the witness into Nullark’s deposit or withdrawal relation. Ledger refinement turns that relation into an authorized pool transition and derives the accounting result over reachable states. The replayable fingerprint fixes reviewed runtime bytes, constructor links, IDs, verifier keys, and template addresses. An authenticated snapshot and finality bind those pieces to live chain state when the deployment theorem is applied.

​
Exact artifact surface

The theorem is fixed to one reviewed artifact set. Similar input shapes do not inherit the result. For both relations, Lean connects:
  • the frozen R1CS rows and their exact file identity;
  • the SnarkJS interpolation QAP in both directions;
  • the verification key and positional public-input order;
  • proof decoding, the verifier MSM, and pairing tuple order;
  • the generated verifier’s accepted runtime path; and
  • the deposit or withdrawal source relation used by the pool model.
The current SDK record carries the same final-zkey identities, runtime ID, template-set ID, and verifier-key identities used by these formal bindings. Current runtime carries the addresses and state checks.

​
What the witness branch proves

An accepted exact deposit proof yields the matching deposit relation, the bound runtime call, and the accepted pool transition. The reachable ledger satisfies the no-inflation inequality before and after that deposit.

​
Successful ETH outflows

The deployment capstone classifies every successful ETH outflow admitted by its exact execution boundary into one of three cases: Starting from a reachable solvent state, every classified successful outflow leaves the modeled pool solvent. Rejected operations and failed ETH transfers preserve the modeled pre-state.

​
Current proof state

​
Assumptions carried by the theorem

The table below names each typed premise at the relevant theorem boundary.

​
Evidence kept separate

​
Reviewable proof roots

The reviewed frozen core includes:
  • deterministic R1CS, QAP, verification-key, and generated-verifier identity checks;
  • negative mutation tests for calldata offsets, public-input count and order, precompile selection, pairing order, and final return behavior;
  • a non-vacuous replayable predeployment fingerprint;
  • focused scans for sorry, admit, new axioms, unsafe, and native proof shortcuts; and
  • axiom reports on the public endpoints, with domain assumptions visible in the theorem signatures.
  • exact_deposit_runtime_acceptance_implies_fund_safety_or_setup_root_break
  • exact_withdrawal_runtime_acceptance_implies_fund_safety_or_setup_root_break
  • exact_replayable_runtime_deployment_fingerprint_nonvacuous
  • successful_deployment_eth_outflow_is_authorized
Read What a Groth16 proof proves for the proof-system model, Current runtime for published runtime identities, and Security status for the live review summary.