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 such as zero-address guards, operator authorization, and public ciphertext ACL checks. An on-chain observer cannot learn whether the sender had enough tokens by watching whether the transaction succeeded.

View OpenZeppelin implementation

Why It 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 Modeled and Proven

The contract model covers all five functions: the three _update paths (transfer, mint, burn), plus transferFrom and setOperator. The specs and proofs use helper-shaped definitions for tryIncrease64WithInit / tryDecrease64WithInit so they cover FHESafeMath's uninitialized-handle branches, matching the Solidity behavior. The contract model uses Verity's source-level internal helpers for Solidity's internal paths such as _update, _transfer, _mint, _burn, and _setOperator. The FHE arithmetic remains inline inside _update, while the proof-side helper definitions make the correspondence withFHESafeMath explicit. 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.

Proof Matrix

All 12 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. Deposit: a successful mint/deposit credits exactly the deposited amount of confidential tokens. setOperator has a separate updates theorem: it writes exactly the caller/operator expiry pair without affecting any other storage.

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

Assumptions

The proofs use zero axioms. The extra hypotheses are proof-side conditions that make the modeled storage case explicit.

• 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.

• hAmount64 / hSupply64 / hBal64amount and modeled euint64 slots are < 2^64

  euint64 representation

  Verity stores modeled euint64 handles as Uint256, so the theorems state the 64-bit range facts that Solidity's FHE type already enforces. Successful mint/deposit proofs also use the initialized-aware FHESafeMath success condition for totalSupply.

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.