> ## Documentation Index
> Fetch the complete documentation index at: https://docs.nullark.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Formal verification

Follow Nullark's artifact-bound fund-safety theorem from exact verifier acceptance to authorization, accounting, and deployment assumptions.

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

```mermaid
%%{init: {"flowchart": {"nodeSpacing": 24, "rankSpacing": 30}}}%%
flowchart TB
  subgraph Core["Nullark's machine-checked Groth16 fund-safety path"]
    direction TB
    ACCEPT["Artifact-bound Groth16 acceptance<br/>The exact runtime uses the bound verification key to check this proof and public-input order on BN254"]
    RESULT{"Type III Groth16 knowledge soundness (AGM)<br/>What can explain that acceptance?"}
    R1CS["Knowledge extraction and exact QAP-to-R1CS<br/>A witness satisfies the frozen circuit constraints"]
    BREAK["Setup-root break<br/>A nonzero check polynomial vanishes at the hidden setup point; the fund-safety path stops"]
    CLAIM["Semantic and ledger refinement<br/>The witness becomes an authorized pool transition, then bounded fund safety"]

    ACCEPT -->|BN254-to-Type III bridge| RESULT
    RESULT -->|knowledge extraction succeeds| R1CS
    RESULT -->|explicit failure branch| BREAK
    R1CS -->|decode the relation and prove accounting| CLAIM
  end
```

**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.

| Relation | Wires | Public signals | Constraints | QAP domain |
| --- | ---: | ---: | ---: | ---: |
| Deposit | 5,941 | 6 | 5,951 | 8,192 |
| Withdrawal | 22,969 | 9 | 22,959 | 32,768 |

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](/reference/current-runtime.md) carries the addresses and state checks.

## What the witness branch proves

### Deposit

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.

### Withdrawal

An accepted exact withdrawal proof yields a note authorization rooted in reachable pool history. Its nullifier starts fresh, is consumed by the transition, cannot authorize the same withdrawal again, and stays unique across the accepted trace. The ledger remains non-inflating and the resulting pool state remains solvent.

## Successful ETH outflows

The deployment capstone classifies every successful ETH outflow admitted by its exact execution boundary into one of three cases:

| Outflow | Required evidence |
| --- | --- |
| Proof-authorized withdrawal | Matching withdrawal relation, reachable backing deposit, rooted note authorization, fresh nullifier, exact accounting transition |
| Fee sweep | Authorized role, bounded accrued fees, exact destination and amount, solvency-preserving state change |
| Excess recovery | Authorized role, value above accounted obligations, exact destination and amount, solvency-preserving state change |

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

| Proof surface | State |
| --- | --- |
| Frozen R1CS semantics | Complete for the reviewed deposit and withdrawal artifacts |
| Exact R1CS-to-QAP correspondence | Complete for both artifact domains |
| Generated-verifier knowledge extraction | Complete as witness or explicit setup-root break under the named cryptographic and runtime assumptions |
| Deposit fund safety | Complete for the exact accepted deposit path |
| Withdrawal fund safety | Complete for authorization, nullifier use, no inflation, and post-state solvency on the exact accepted withdrawal path |
| Deployment outflow classification | Complete under authenticated state, finality, setup evidence, and exact compiler and MegaEVM source transport |
| Replayable deployment fingerprint | Complete as a predeployment template for canonical runtimes, constructor links, template addresses, IDs, and verifier keys |
| Changed circuits, keys, or runtimes | A new artifact set becomes a new proof target and repeats the binding and review |

## Assumptions carried by the theorem

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

| Boundary | Assumption |
| --- | --- |
| Algebraic proof model | Type III AGM coefficient representation and the pinned Groth16 knowledge-soundness model |
| Setup and verification key | Exact SRS and verification-key interpretation, plus group and pairing fidelity at the sampled setup point |
| BN254 and MegaEVM | Canonical field encoding, curve negation, group operations, pairing behavior, and the modeled precompile interface |
| Runtime transport | Exact calldata and public-input binding, generated-verifier call transport, and the pool source transition certificates |
| History and hashes | Reachable deposit history and pair-scoped collision-resistance assumptions for the exact commitment, nullifier, and context links used by the proof |
| Ceremony | At least one honest contribution and the stated entropy custody and deletion condition when the setup-backed deployment theorem is applied |
| Deployment | Compiler and runtime identity, authenticated code and state, and finality when the theorem is instantiated against a live deployment |

## Evidence kept separate

| Surface | Evidence path |
| --- | --- |
| Browser proving and witness construction | SDK tests, artifact validation, browser builds, and end-to-end execution |
| Wallet, recovery, and submission UX | Integration tests, provider review, and operational controls |
| Privacy and anonymity | [Privacy boundaries](/security/privacy-boundaries.md) and separate privacy analysis |
| Live code, state, and finality | [Current runtime](/reference/current-runtime.md), code identity checks, state authentication, and chain finality |
| Any replacement artifact set | Fresh generation, exact identity checks, focused Lean builds, escape scans, and independent review |

## 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.

### Lean theorem endpoints

- `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](/security/proof-system.md) for the proof-system model, [Current runtime](/reference/current-runtime.md) for published runtime identities, and [Security status](/security/status.md) for the live review summary.