Formal verification
What the Lean models of the circuits prove, what they assume, what they show cannot be proved, and what the Kani harnesses and Lean models check on the chain side.
Umbra's circuits are modelled in Lean 4 and the models are machine-checked. They prove the properties that matter most for money, such as no minting, under stated assumptions. The models are written by hand, so they show what the constraints imply, not that the Circom compiles to exactly those constraints.
What is modelled
The Lean development under circuits/zk/lean4 has three libraries, built together with just verify-circuits-lean. They differ in how closely they follow the circuits.
UmbraCircuits
The shared library models the building blocks every circuit uses: field aliasing and bit decomposition, the 53-slot public fold, note kinds, Merkle folds, indexed trees, Shamir sharing, fee rates and rounding, batch append and registration. It is the most abstract of the three. Poseidon is an opaque function, so the theorems hold for any hash that meets the stated assumptions, and say nothing about Poseidon's internals.
TransactionCircuit
This library follows the transaction circuit constraint group by constraint group, from the spender's identity through the fee allocation to the sender record and the zones. Hashes enter as a hypothesis, a family of functions the theorems are stated over, rather than as Poseidon itself. It is the library the main money theorems below come from.
EscapeHatch
This library models the escape-hatch circuit constraint by constraint, including its non-membership check. It also holds the field definitions and the aliasing theorems the other libraries reuse. As the callout further down says, it models an earlier version of the circuit.
What is proved
For the transaction circuit, under the range bounds the circuit enforces, the main theorems are these.
no_minting. For each token, the new notes cannot hold more than the spent notes and deposits brought in.
no_unfunded_withdrawal. A withdrawal lane is always covered by spent notes or deposits of the same token.
fees_are_funded and the_tip_is_funded. Protocol fees and the relayer's tip come out of the transaction's own value, never from nowhere.
the_nullifier_run_has_no_repeat. Each published nullifier appears exactly once among the three.
the_spend_leaves_one_zone and zone_authorisation_is_conditional. Real inputs share one zone, and zone 0 opts out of the zone signature entirely.
the_record_describes_the_transaction. Two accepted transactions with the same sender record have the same record inputs and outputs, so the record pins down the transaction's assets slot by slot.
Production-shape theorems. production_user_spend_is_satisfiable and its siblings for program-owned and mixed spends show that the real 3×3×2×2 shape admits honest transactions. Without them, a set of constraints that nothing could satisfy would make every soundness theorem trivially true.
For the escape hatch, escape_sound collects escape_value_sound, escape_nullifier_unspent and escape_disclosure_faithful: the payout is backed by one real unspent note, and the disclosed fields are that note's fields. The note's version is not disclosed, and escape_withheld_version_bound shows it is still pinned to that same note.
What the proofs show cannot hold
Some theorems prove limits rather than guarantees. They exist so that nobody relies on a property the circuit does not have.
conservation_needs_the_range_bounds. Without the 64-bit range checks, field arithmetic would let value wrap around the modulus, so the conservation equation means nothing without them.
the_lane_mint_limbs_are_unbounded. The circuit does not range-check the token-address halves of deposit and withdrawal lanes. The shielded pool program supplies them from real accounts, which is what closes the gap.
the_fee_is_an_interval_not_a_number. For a destination funded by other owners, the charge depends on how the prover allocates sources to it. It lies between the cheaper and the dearer of the two rates that could apply (deposit or transfer for a new note, withdraw or pass-through for a lane), times the destination's amount. The fee is pinned only to that interval, and the prover may always pay more.
comparator_admits_value_less_than_itself, gap_check_can_straddle_a_spent_nullifier and full_width_is_exploitable (in the escape-hatch library). A comparison over full 254-bit values aliases in the field: a value can be shown to be less than itself, and a non-membership gap can be made to straddle a nullifier that is in the tree. These are the reason the circuits decompose values into canonical limbs before comparing them.
Assumptions
Every result rests on these, and they are stated in the code rather than proved.
model_matches_circom. The hand-written model is the circuit. It is an axiom with no content, cited by the_model_is_assumed_to_be_the_circuit so that the assumption shows up wherever it is used.
poseidon_injective. Poseidon is treated as collision-free on inputs of equal length. Real Poseidon cannot be injective, so this is an idealisation of collision resistance.
poseidon_prf_indistinguishable, babyjubjub_discrete_log_hard and keccak_collision_resistant. Named placeholders for standard cryptographic assumptions. Each is stated as an axiom with no content, so it records the assumption without being usable in a proof.
fieldOrder_prime. The escape-hatch library takes the primality of the BN254 scalar field order as an axiom rather than certifying it, and the transaction library depends on it through the shared field definitions.
The TransactionCircuit library pins its axiom footprint: its audit file prints the axioms each main theorem depends on and fails the build if that list changes. The UmbraCircuits audit prints them without pinning.
The chain side
The Rust crates behind the shielded pool program's trees and staging buffers are checked with Kani, a model checker for Rust. Its harnesses explore every input within stated bounds and check that assertions hold for all of them. Three of the crates also have Lean models, and the batched proof check and the shielded pool program each have a Lean library of their own.
The staging buffer
The turnstile crate is the staging buffer (the code calls it the turnstile) behind nullifiers, registrations and fee nullifiers. Its Kani harnesses establish that a key cannot be staged twice, in one buffer or across both; that a stale root is refused once its buffer retires; that the watermark only rises; that a commit with the wrong root or the wrong batch chain is refused; that a non-canonical key is refused and writes nothing; and that bounded operations never panic. Its Lean model proves that, in every state reachable from the start, no key is staged twice, and that retiring a buffer never lowers the watermark. A second part of the model treats a buffer as the list of keys it stores, in staging order, and proves that folding each batch's stored keys when the batch commits gives the same chain as folding each key into its batch's chain as it is staged, for any fold function and any keys staged into an empty buffer. The build fails if that theorem's axiom footprint changes. Another module models the staging buffer's Bloom index. It proves the mixing function is a bijection on 64-bit words, so two keys that differ in exactly one of their four words get different first index words and different second chains, before the step is made odd; it also proves the step is always odd. just verify-turnstile-lean builds the model.
The incremental Merkle tree
The incremental-merkle-tree crate is the append-only tree the shielded pool program uses for its note, identity and fee trees. Its Kani harnesses establish that the incremental root equals a naive recomputation, for mixed arity too; that indices are sequential and the tree refuses inserts once full; that honest paths always verify; that padded or out-of-range paths are refused; that the recent-root ring holds exactly its window; and that batched appends fold the same as one-at-a-time appends. Its Lean model proves the batched fold, with and without the group seal, equals folding one leaf at a time.
The pending set
The pending-set crate is the Bloom filter and key store behind the staging buffer. Its harnesses establish that every filter index is within the bit array; that setting a bit disturbs no other bit and is idempotent; that an inserted key is found and a duplicate insert changes nothing; that membership matches an exhaustive oracle; that after a wipe no key is found and the set accepts inserts again; and that a stored set loads only when its recorded length is sane and its regions do not overlap. Its Lean model, built with just verify-pending-set-lean, proves that membership is exact whatever bit positions a key is given: a held key is always found and an absent key never is, through every sequence of inserts and wipes. So the choice of index can cost compute but never let a staged key through. It also proves that with an odd step a key's probes land on distinct bits, and that a lookup testing no more probes than the inserts used still finds every held key; one testing more could miss a key, which is why a change to the probe count comes with a new account layout version.
The batched proof check
process_3x3x2x2 checks its transaction proof, its nullifier-freshness proof and the combined attester signature with one pairing, weighting the second proof by a random scalar r and the signature by a random scalar s, both drawn from a hash of every value the submitter supplied and cut to 253 bits. The groth16-verifier crate's Lean library models that check with the curve groups as vector spaces over the scalar field, which is what they are once the pairing syscall has refused every point outside its prime-order subgroup, and the pairing as a bilinear map. Under a shared setup, where both keys have the same α, β and γ and γ is the G2 generator, it proves that the combined check is the first proof's check plus r times the second's plus s times the signature's, so it passes whenever all three would. It also proves that when any one of the three would fail, at most 2²⁵³ of the 2²⁵³ × 2²⁵³ possible weight pairs make the combined check pass: a forged batch survives one draw of the weights with probability at most 2⁻²⁵³. just verify-groth16-batch-lean builds it, and the build fails if any theorem's axiom footprint changes.
The shielded pool program
The shielded pool program's Lean library, built with just verify-shielded-pool-lean, models its checks of fixed accounts. The program's build derives, for its own program IDs, the canonical address and bump of each account it checks on every value transaction, and a check passes at once when the account's address and stored bump equal the build's entry; otherwise it derives the address as before. With the derivation left as an arbitrary function, the library proves that this check accepts exactly the accounts the derivation accepts whenever each entry is one the derivation produces, which the build asserts of every entry; and that the vault authority, checked at its entry's own bump, admits its own address and no other. That each call site consults the entry for the seeds it derives is a property of the program's code, which its litesvm suite tests.
The library also models the cached committee key. With the curve addition and the refusal of a degenerate sum as arbitrary functions, and the keys each create or refresh reads left arbitrary because records may change between any two of them, it proves that every cache any sequence of creates and refreshes can leave holds the sum of exactly the four keys it stores, and never a degenerate sum. So when a cache's keys are the keys a transaction reads, its sum is the sum of those keys: using it never changes the key the combined attester signature is checked under. It also models the transaction's choice between the cached sum and its own: whatever account the transaction names for the cache, the key it checks the signature under is the sum of the keys it read.
The library also models the fee store, where a value transaction stages its fee commitments until an insert appends them to the fee commitment tree. With the leaves an entry becomes left as an arbitrary function of its index and contents, it proves that after any sequence of stages and inserts the tree holds exactly the leaves of the entries inserted so far, in the order they were staged, so it is always a prefix of the tree immediate appends would have built; that each entry's leaves take the positions they were staged for; and that a stage into a full store, which inserts the oldest entry first, never lets the store exceed its capacity. The ring the program keeps the staged entries in is covered by the state crate's tests rather than by this model.
The guardian node registry and the Nitro attestation verifier programs have Lean models of their own, which lie outside the proofs this page covers.
What is not verified
- The link between the Circom source and the Lean models.
- The shielded pool program's handlers, beyond the state crates and the models above.
- The off-chain services: guardian nodes, screener, fee enclave, data endorser, relayer, indexer.
- The cryptographic primitives themselves, which are assumed.
Related
Last updated
Merge circuit
A circuit that combines up to eight of one owner's notes into one, written for the EVM port of the pool and not used by the Solana program.
Register
What happens when you register, from deriving your keys to the shielded pool appending your identity commitment, including what each attester checks and what becomes public.