ERC-7984 Confidential Token Invariants

ERC-7984 is a confidential fungible token standard co-developed by Zama and OpenZeppelin for the fhEVM. All balances and transfer amounts are encrypted as euint64 ciphertext handles using Fully Homomorphic Encryption. Users can hold, send, and receive tokens without revealing their balances to anyone, including validators.

The main 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 2⁶⁴ (not 2²⁵⁶), 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.

View OpenZeppelin implementation

Why this matters

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 that protects users also hides accounting errors. If a bug caused tokens to silently vanish, there would be no on-chain signal. Formal verification closes that gap: if the invariants hold for all inputs, the accounting is correct regardless of what the ciphertexts contain.

How this was proven

The contract model covers all five functions: the three _update paths (transfer, mint, burn), plus transferFrom and setOperator. Arithmetic uses tryIncrease64 / tryDecrease64, matching the Solidity exactly. Because euint64 values are modeled as Uint256 rather than a bounded type, some theorem statements carry explicit < 2^64 preconditions on inputs and balances; these reflect what the FHE type enforces at the contract level, not additional contract assumptions. _operators is modeled as a native nested mapping via storageMap2. blockTimestamp is passed as an explicit parameter to transferFrom for the operator expiry check.

Token conservation is straightforward to state: 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.

Most theorems handle the two branches of FHE.select separately: the sufficient-balance path and the insufficient-balance path. Each branch reduces to a concrete arithmetic statement that the proof checker verifies automatically. The non-revert theorem works differently: instead of branching on balance, it goes through every require in the function and shows each one is already satisfied by the preconditions. Since no require checks whether the balance is sufficient, balance never enters the picture.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Zama.ERC7984ConfidentialToken.Proofs

Proof status

All 11 theorems are proven across five functions. Every task file is sorry-free.

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. setOperator has a separate updates theorem: it writes exactly the caller/operator expiry pair without affecting any other storage.

Assumptions

The proofs use zero axioms. Two hypotheses encode plaintext preconditions that the contract checks explicitly.

• hInitbalanceInitialized[from] != 0

  FHE.isInitialized gate

  The sender's balance has been initialized. The contract checks FHE.isInitialized(fromBalance) and reverts with ERC7984ZeroBalance if not, meaning the transfer is from an account that has received tokens before.

• hDistinctsender != recipient

  Storage model

  Sender and receiver are different addresses. Required because the model reads and writes balance slots independently. A self-transfer is a separate (trivial) case.

View specs in LeanView contract model in Lean

Learn more

ERC-7984: The Confidential Token Standard Explained, by Zama.

OpenZeppelin Confidential Contracts, the upstream implementation.

What is a formal proof? A short explanation for non-specialists.