Nullark machine-checks one promoted withdrawal fund-safety theorem in Lean 4. The page below is its current summary. The dated report carries the complete public claim, evidence tables, artifact commitments, and trust boundary.

Download formal verification report

Read the 20-page report dated 4 September 2026.

​
Verified claim

Given the documented artifact, runtime, deployment, and Groth16 premises, an accepted successful withdrawal from a solvent state produces an authorized, single-use result with exact user-payout, relay-fee, and protocol-fee conservation; preserved solvency; and rollback when a required payout fails, or it yields an explicit Groth16 setup-root break.
In short: an accepted, successfully executed withdrawal is fund-safe unless a stated real-world binding is false or Groth16/setup security is defeated.

​
What is machine-checked

  • exact public-input decoding, ordering, and canonical field checks;
  • frozen withdrawal R1CS satisfaction and QAP correspondence;
  • symbolic Type III Groth16 knowledge extraction under explicit algebraic premises;
  • deposited-note authorization, accepted-root membership, and nullifier single use;
  • three-way value conservation across user payout, relay fee, and protocol fee;
  • exact accounting and state changes, preserved solvency, and atomic rollback when either required payout fails.
Promoted endpoint: Nullark.Claims.promoted_fund_safety_or_setup_root_break.

​
Current evidence

Deployment evidence is an exact RPC observation. RPC authenticity, authenticated state proof, and finality remain external boundaries.

​
Where the theorem stops

Result depends on exact artifact and runtime correspondence, compiler and EVM fidelity, BN254 and pairing behavior, authenticated deployment state, and Groth16/setup security. Scope covers withdrawal fund safety only. Anonymity, wallet-recovery correctness, frontend behavior, relayer availability, and other product properties remain separate surfaces. Read Privacy boundaries, Recovery-note safety, and Security status. PDF SHA-256: 6c91407196506e65680beb0c059d79e4a874899ec7c0962203c99029d49539de.