+ ERC-20 transfer +
+ + {/* Scenario: enough funds */} ++ + Alice has 100, sends 50 to Bob +
++ ✓ Transfer succeeds +
++ + Alice has 30, sends 50 to Bob +
++ ✕ Transaction reverts. Everyone sees it failed. +
++ ERC-7984 transfer (encrypted) +
+ + {/* Scenario: enough funds */} ++ + Alice has 100, sends 50 to Bob +
++ ✓ 50 moved, but amounts stay hidden +
++ + Alice has 30, sends 50 to Bob +
++ ✓ Tx succeeds, but 0 moved. No one can tell it failed. +
++ ERC-7984 never reverts on insufficient balance. Reverting would reveal + that the sender doesn't have enough funds. +
+
+ {formal}
+
+ ))}
+ + Tokens are never created or destroyed by a transfer. +
++ Sufficient transfers move exactly the requested amount. +
++ Insufficient transfers change nothing and never revert. +
+
+ euint64 ciphertext
+ handles using Fully Homomorphic Encryption. Users can hold, send,
+ and receive tokens without revealing their balances to anyone,
+ including validators.
+
+ The key semantic difference from ERC-20: because the contract
+ cannot branch on encrypted values, transfers with insufficient
+ balance silently transfer zero instead of reverting.{' '}
+ FHE.select picks
+ the result without revealing which path was taken. Arithmetic wraps
+ at 264 (not 2256), and{' '}
+
+ FHESafeMath.tryIncrease
+ {' '}
+ /{' '}
+ tryDecrease{' '}
+ detect overflow and underflow without revealing whether they
+ occurred.
+
+ We also proved that a transfer never reverts based on + balance sufficiency. The only reverts come from plaintext checks + (zero address, uninitialized balance). An on-chain observer + cannot learn whether the sender had enough tokens by watching + whether the transaction succeeded. +
+
+
+ In a standard ERC-20, a broken transfer reverts and the user sees + the error. In ERC-7984, a broken transfer looks identical to a + successful one from the outside. If the accounting logic had a + bug, tokens could silently appear or vanish with no on-chain + signal that anything went wrong. +
++ The confidentiality guarantee cuts both ways: it protects user + privacy, but it also hides accounting errors. Formal verification + is the way to close this gap. If the invariants hold for all + possible inputs, the accounting is correct regardless of what the + ciphertexts contain. +
+
+ The proofs cover the core accounting of all four state-mutating
+ functions:{' '}
+ transfer,{' '}
+ transferFrom,{' '}
+ mint, and{' '}
+ burn. Eight
+ theorems verify: balance conservation across transfers,
+ correct behavior for both sufficient and insufficient balances,
+ supply isolation from transfers, mint/burn supply correctness,
+ overflow protection, and non-revertability on insufficient
+ balance (the contract-level non-leakage guarantee).
+
+ Out of scope: the FHE encryption layer (handled by
+ Zama's TFHE library), the ACL system (
+ FHE.allow
+ — controls ciphertext access, not balances),
+ cryptographic proof verification (
+ fromExternal{' '}
+ + inputProof
+ ), off-chain gateway decryption, and receiver callbacks (
+ AndCall{' '}
+ variants). These are separate systems that do not affect
+ balance state.
+
+ ERC-7984 operates on encrypted values, but FHE is{' '}
+ homomorphic: if{' '}
+ f(a, b) = c on
+ plaintext, then{' '}
+
+ f(enc(a), enc(b)) = enc(c)
+ {' '}
+ on ciphertexts. This means proving a property on plaintext values
+ is equivalent to proving it on ciphertexts. Zama's TFHE
+ library provides the cryptographic guarantee; we verify the
+ logic.
+
euint64{' '}
+ →{' '}
+ Uint256 with
+ explicit{' '}
+ mod 2^64{' '}
+ wrapping
+
+ FHE.select(cond, a, b)
+ {' '}
+ →{' '}
+
+ if cond then a else b
+
+
+ FHE.add / FHE.sub
+ {' '}
+ → wrapping arithmetic at{' '}
+ 2^64
+
+ The contract was modeled in{' '}
+ _update:
+ transfer (from and to are non-zero), mint (from is zero), and
+ burn (to is zero). Each path uses{' '}
+ tryIncrease64 /{' '}
+ tryDecrease64{' '}
+ for overflow-safe arithmetic, matching the Solidity exactly.
+ {' '}The only structural simplification is the operator mapping:
+ Verity does not support nested mappings, so operator expiry
+ is passed as a function parameter instead of read from{' '}
+
+ _operators[holder][spender]
+ .
+
+ How do you prove tokens are conserved across a confidential
+ transfer? You show that{' '}
+
+ balances[from] + balances[to]
+ {' '}
+ is the same before and after, for all inputs. If the
+ sender has enough, exactly{' '}
+ amount moves. If
+ not,{' '}
+ select picks
+ zero, both balances write back unchanged, and the sum is
+ trivially preserved.
+
+ All proofs are verified by Lean 4's kernel. If any step + were wrong, the code would not compile. +
+
+ If the build succeeds, the proofs are correct.{' '}
+
+ All 8 theorems are proven. Every task file is{' '}
+ sorry-free.
+
| + Function + | ++ Conservation + | ++ Sufficient + | ++ Insufficient + | ++ No revert + | ++ Supply + | ++ Overflow + | +
|---|---|---|---|---|---|---|
| transfer | ++ proven + | ++ proven + | ++ proven + | ++ proven + | ++ proven + | ++ — + | +
| mint | ++ — + | ++ proven + | ++ — + | ++ — + | ++ proven + | ++ proven + | +
| burn | ++ — + | ++ proven + | ++ — + | ++ — + | ++ proven + | ++ — + | +
+ Conservation: sender + receiver sum preserved.{' '} + Sufficient: correct amount moves when balance + covers it. Insufficient: no change when balance + is too low. No revert: transfer does not revert + on insufficient balance. Supply: totalSupply + changes correctly + (or not at all for transfers). Overflow: mint + detects uint64 overflow and mints nothing. +
+
+ The proofs use zero axioms. The theorems require these
+ hypotheses, which encode constraints about valid{' '}
+ euint64 state:
+
euint64 values.
+ In the real contract, the FHE layer enforces this: ciphertext
+ handles always encrypt values in{' '}
+ [0, 2^64).
+ euint64. Same
+ reasoning: all stored ciphertext handles decrypt to values in
+ range.
+ euint64.
+ euint64.
+ Required by mint and burn proofs.
+
+ FHE.isInitialized(fromBalance)
+ {' '}
+ and reverts with{' '}
+
+ ERC7984ZeroBalance
+ {' '}
+ if not. This hypothesis encodes that the transfer is from an
+ account that has received tokens before.
+ 2^64 and no
+ individual balance can exceed supply.
+
+
+
+
+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +
+