From f387c4e68632bc1d13dd019b40bd21750099d0c7 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Thu, 16 Apr 2026 16:44:28 +0100 Subject: [PATCH] feat: add zama ERC-7984 article --- .../research/ConfidentialTransferDiagram.jsx | 116 ++++ components/research/ZamaGuarantee.jsx | 107 ++++ data/research.js | 10 + .../zama-erc7984-confidential-token.jsx | 504 ++++++++++++++++++ 4 files changed, 737 insertions(+) create mode 100644 components/research/ConfidentialTransferDiagram.jsx create mode 100644 components/research/ZamaGuarantee.jsx create mode 100644 pages/research/zama-erc7984-confidential-token.jsx diff --git a/components/research/ConfidentialTransferDiagram.jsx b/components/research/ConfidentialTransferDiagram.jsx new file mode 100644 index 0000000..3837a17 --- /dev/null +++ b/components/research/ConfidentialTransferDiagram.jsx @@ -0,0 +1,116 @@ +export default function ConfidentialTransferDiagram({ className = '' }) { + return ( +
+
+ {/* ERC-20 */} +
+

+ ERC-20 transfer +

+ + {/* Scenario: enough funds */} +
+

+ + Alice has 100, sends 50 to Bob +

+
+
+ Alice + 100 → 50 +
+ → +
+ Bob + 0 → 50 +
+
+

+ ✓ Transfer succeeds +

+
+ + {/* Scenario: not enough funds */} +
+

+ + Alice has 30, sends 50 to Bob +

+
+
+ Alice + + 30 + +
+ ✕ +
+ Bob + 0 +
+
+

+ ✕ Transaction reverts. Everyone sees it failed. +

+
+
+ + {/* ERC-7984 */} +
+

+ ERC-7984 transfer (encrypted) +

+ + {/* Scenario: enough funds */} +
+

+ + Alice has 100, sends 50 to Bob +

+
+
+ Alice + 🔒 → 🔒 +
+ → +
+ Bob + 🔒 → 🔒 +
+
+

+ ✓ 50 moved, but amounts stay hidden +

+
+ + {/* Scenario: not enough funds */} +
+

+ + Alice has 30, sends 50 to Bob +

+
+
+ Alice + 🔒 → 🔒 +
+ → +
+ 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. +

+
+ ) +} diff --git a/components/research/ZamaGuarantee.jsx b/components/research/ZamaGuarantee.jsx new file mode 100644 index 0000000..76ddc92 --- /dev/null +++ b/components/research/ZamaGuarantee.jsx @@ -0,0 +1,107 @@ +import { useState, useEffect, useRef } from 'react' +import { ExternalLinkIcon } from './ExternalLink' + +const FORMAL_INVARIANTS = [ + 'balances\u2032[from] + balances\u2032[to] = balances[from] + balances[to]', + 'balance \u2265 amount \u2192 balances\u2032[from] = balances[from] \u2212 amount \u2227 balances\u2032[to] = balances[to] + amount', + 'balance < amount \u2192 balances\u2032[from] = balances[from] \u2227 balances\u2032[to] = balances[to]', + 'balance < amount \u2192 \u00ACreverts', + '\u2200 transfer, totalSupply\u2032 = totalSupply' +] + +export default function ZamaGuarantee() { + const [showEnglish, setShowEnglish] = useState(true) + const timerRef = useRef(null) + + useEffect(() => { + timerRef.current = setTimeout(() => setShowEnglish(false), 5000) + return () => clearTimeout(timerRef.current) + }, []) + + const handleToggle = () => { + if (timerRef.current) { + clearTimeout(timerRef.current) + timerRef.current = null + } + setShowEnglish((prev) => !prev) + } + + return ( +
+ + +
+
+ {FORMAL_INVARIANTS.map((formal, i) => ( + + {formal} + + ))} +
+
+
+

+ Tokens are never created or destroyed by a transfer. +

+

+ Sufficient transfers move exactly the requested amount. +

+

+ Insufficient transfers change nothing and never revert. +

+
+
+
+ +
+ + View Lean + + +
+
+ ) +} diff --git a/data/research.js b/data/research.js index 468b89d..60012f2 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'zama-erc7984-confidential-token', + title: 'ERC-7984 Confidential Token Invariants', + subtitle: + 'Formally verified accounting properties of the Confidential Token Standard.', + description: + 'How we proved transfer conservation, mint/burn correctness, and overflow protection for ERC-7984 (Zama fhEVM + OpenZeppelin) using Verity and Lean 4.', + date: '2026-04-16', + tag: 'Case study' + }, { slug: 'stream-recovery-claim', title: 'StreamRecoveryClaim Accounting Invariants', diff --git a/pages/research/zama-erc7984-confidential-token.jsx b/pages/research/zama-erc7984-confidential-token.jsx new file mode 100644 index 0000000..80b3814 --- /dev/null +++ b/pages/research/zama-erc7984-confidential-token.jsx @@ -0,0 +1,504 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import ZamaGuarantee from '../../components/research/ZamaGuarantee' +import ConfidentialTransferDiagram from '../../components/research/ConfidentialTransferDiagram' +import Disclosure from '../../components/research/Disclosure' +import CodeBlock from '../../components/research/CodeBlock' +import ExternalLink from '../../components/research/ExternalLink' +import Hypothesis from '../../components/research/Hypothesis' +import { getSortedResearch } from '../../lib/getSortedResearch' + +const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark +cd verity-benchmark +lake build Benchmark.Generated.Zama.ERC7984ConfidentialToken.Tasks.TransferConservation` + +const UPSTREAM_STANDARD = + 'https://www.zama.org/post/erc-7984-the-confidential-token-standard-explained' + +const UPSTREAM_CONTRACTS = + 'https://docs.openzeppelin.com/confidential-contracts/token' + +const VERITY_CONTRACT = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Zama/ERC7984ConfidentialToken/Contract.lean' + +export default function ZamaERC7984Page() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'zama-erc7984-confidential-token' + ) + + return ( + <> + + + ERC-7984 Confidential Token Invariants | Research | LFG Labs + + + + +
+ + +
+

+ ERC-7984 Confidential Token Invariants +

+
+ + {/* The Guarantee */} +
+ +

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

+

+ + View OpenZeppelin implementation + +

+
+ + {/* Why this matters */} +
+

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

+ +
+ + {/* How this was proven */} +
+

+ How this was proven +

+

+ 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{' '} + Verity from + OpenZeppelin's{' '} + + confidential-contracts + {' '} + implementation. The model captures the three paths through{' '} + _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. +

+ + {VERIFY_COMMAND} +

+ If the build succeeds, the proofs are correct.{' '} + + Source repository + +

+ +
+ + {/* Proof status */} +
+

+ Proof status +

+

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

+
+ + {/* Assumptions */} +
+

+ Assumptions +

+

+ The proofs use zero axioms. The theorems require these + hypotheses, which encode constraints about valid{' '} + euint64 state: +

+
    + + Transfer, mint, and burn amounts are valid{' '} + euint64 values. + In the real contract, the FHE layer enforces this: ciphertext + handles always encrypt values in{' '} + [0, 2^64). + + + Sender balance is a valid{' '} + euint64. Same + reasoning: all stored ciphertext handles decrypt to values in + range. + + + Receiver balance is a valid{' '} + euint64. + + + Total supply is a valid{' '} + euint64. + Required by mint and burn proofs. + + + The sender's balance has been initialized. The real + contract checks{' '} + + FHE.isInitialized(fromBalance) + {' '} + and reverts with{' '} + + ERC7984ZeroBalance + {' '} + if not. This hypothesis encodes that the transfer is from an + account that has received tokens before. + + + Sender and receiver are different addresses. Required because + the model reads and writes balance slots independently. A + self-transfer is a separate (trivial) case. + + + Receiver balance does not overflow after adding the transfer + amount. Only needed for the conservation theorem. In practice, + this holds because total supply is bounded by{' '} + 2^64 and no + individual balance can exceed supply. + +
+

+ + View specs in Lean + + + View contract model in Lean + +

+
+ + {/* Learn more */} +
+

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

+
+ + {otherResearch.length > 0 && ( +
+

+ More research +

+
+ {otherResearch.map((r) => ( + + ))} +
+
+ )} +
+ + + ) +}