Nullark uses Lean to check the fund-moving rules behind deposits and withdrawals. Reliable coverage depends on matching every theorem to the same constraints, verifier, runtime code, and deployment people use.

​
What is different here

Nullark’s differentiator is cross-layer traceability. The layers stay in one proof path, leaving less room for a correct theorem about the wrong artifact. Every arrow needs its own evidence. An unfinished arrow stays unfinished.

​
What has been checked

​
How a result earns its claim

  • Exact artifacts. Constraints, generated verifier data, bytecode, hashes, and public-input order must agree.
  • A real path. Positive cases show that the claimed branch can happen. Negative mutations reject nearby unsafe cases.
  • Auditable trust. Load-bearing results are checked for unfinished proofs and their transitive Lean axioms are printed for review.
  • A named boundary. Model, constraints, verifier, runtime, and deployment are separate levels. Moving between levels requires new evidence.
External assumptions remain visible, including Groth16 soundness, setup security, compiler correctness, BN254 and MegaETH execution behavior, and authenticated deployment state.

​
Where it stands today

Lean currently covers pinned constraint semantics, verifier identity, and selected runtime behavior. The end-to-end deposit and withdrawal proof is still under review. Browser, wallet, relayer, ceremony, privacy, and deployment checks continue in their own evidence tracks. Read Published security status for the current claim state and What a Groth16 proof proves for the proof-system assumptions.