> For AI agents: the documentation index is at https://docs.umbraprivacy.com/llms.txt, and every page is available as Markdown at its URL with .md appended. # Formal verification (/docs/proofs/formal-verification) 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 - [The transaction circuit](https://docs.umbraprivacy.com/docs/proofs/transaction-circuit): The constraints the Lean model follows. - [Value conservation](https://docs.umbraprivacy.com/docs/state/value-conservation): The per-token equation no_minting is about. - [Preventing double spends](https://docs.umbraprivacy.com/docs/state/double-spend): What the staging buffer harnesses protect. - [Audits and verification](https://docs.umbraprivacy.com/docs/security/audits): Where this sits among the security work. Last updated 12 October 2026