ethereum

New EIP! Post-Quantum PeerDAS and Variable-Size Blobs 🔗 EIPs#12604 Highlights: - Replaces KZG commitments/proofs in PeerDAS with per-blob Keccak-256 Merkle commitments and Merkle authentication paths, aiming for post-quantum-friendly assumptions and no trusted setup. - Introduces a LeanDA STARK “guest program” that (1) recomputes each blob’s Merkle root, (2) checks Reed–Solomon encoding relations, and (3) proves the published commitments match the blob data; the proof is referenced via EIP-8288 dependency frames using a reserved LEANDA_SCHEME. - Enables variable-size blobs: blob byte lengths must be power-of-two between 2,048 and 524,288, divisible by 128 columns; blobs still have 128 cells, so cell size varies by blob size. - Changes execution-layer blob-carrying transactions (EIP-8141 frames) to carry signed blob_commitments = (merkle_root, byte_length) instead of blob_versioned_hashes; BLOBHASH derives a new PQ versioned hash from root+length with version byte 0x02. - Updates networking and limits: defines eth/73 “sparse blobpool” cell exchange using variable-size cells plus optional Merkle paths; adds engine_getBlobsV5 returning cells and paths; redefines blob gas as blob_byte_length + fixed internal-node charge (127*32) and scales EIP-7892 schedules accordingly, while keeping PeerDAS custody/sampling/recovery rules unchanged. ELI5: Today, Ethereum “blobs” use a math trick (KZG) that could be broken by a future quantum computer, and blobs must be one fixed size. This proposal switches to “hash trees” (Merkle trees) plus a quantum-resistant proof (a STARK) to show the blob is well-formed, and it lets blobs come in different power-of-two sizes so people can publish exactly the amount of data they need.

I wrote a draft EIP to add expiry to 7702 authorizations on the heels of the Binance hack EIPs#12601

We now have a first working version of leanXMSS in Lean4, available in EthLib! This is the XMSS implementation we're planning to use for EIP-8450, Ethereum's post-quantum validator public key registry. github.com/ethereum/EthLib/tree/master/EthLib/Cry…

[ethresear.ch] [Layer 2/ZK Rollup] Ephemeral Rollup: The New "L1.5" of Ethereum namnc October 28 Ephemeral Rollup: The New “L1.5” of Ethereum TLDR; Ethereum’s core job has always been verifying state transitions. While rollups made that verification succinct, they at the same time hold their users’ state, which is why every rollup needs an exit. Native account abstraction (EIP-8141 and related EIPs) and proof aggregation are making it practical to keep compute and state apart. We call this L1.5, albeit it is perhaps more an architectural pattern than a layer. In the pattern we are talking about: a) The wallet keeps the user’s own state, b) L1 keeps the shared state and verifies every transition, and c) the compute in between is done by whoever takes the job without holding any state the next job needs, and d) state changes settle directly on L1. The idea is not new: Relayers, builders and keypers have already done parts of this kind of job, and FOCIL’s includers will be next. What is new is the timing, “now and next”, as this becomes practical to build. We aim only to give a rough conceptualization of it in this post. Introduction Ethereum first verified state transitions by re-executing them. Rollups added succinct verification, where a fraud or validity proof lets L1 accept a batch without re-executing it. But a rollup also holds its users’ state. The state is kept in the rollup’s contract and only the rollup can change it, so users need an exit to leave. This was a deliberate choice, since rollups were built to scale Ethereum and at the time keeping the state off L1 was the efficient way to do that. Rollups, as the 2021 rollup guide puts it, “move computation (and state storage) off-chain”. Keeping user state on L1 would have been costly: 1) Each user’s transition had to be verified on L1 one at a time, which was expensive, and 2) only an account’s key holder could send a transaction, so someone (a relayer or a sequencer) had to submit each transition and pay its gas. EIPs that are scheduled or proposed now address both aforementioned issues: 1) With frame transactions a contract can send and pay for its own transaction, and 2) with proof aggregation each proof is checked once in the mempool and the block carries one proof for all of them. This makes it practical for an application to keep its state on L1 and hand the computation to whoever is available to do it. We attempt to conceptualize this new pattern in two parts: Part 1 describes the pattern, and Part 2 for its context. Part 1: the pattern Three places for state wallet : the user's own state, in the clear, and the secrets that open it L1 : shared and global state a commitment per piece of user state (its provenance) a "used" marker per spent piece (a nullifier) the verifier of every transition L1.5 : f(L1 state, user's inputs) -> (new state, proof) for one transaction or one round; keeps nothing the next job needs This is the commit-and-prove design that L2s use, except that the commitment is on L1 and the opening is in the wallet. L1 keeps only what it needs to check the next transition, the wallet keeps everything else, and L1.5 does solely the computation. Reality check: Private rollups already keep notes in the wallet. In Aztec, the user’s PXE runs on the client and stores the notes, and a transaction sends “new note commitments and nullifiers” to the sequencer, which adds them to the rollup’s trees. In L1.5 the commitments and nullifiers go to L1 directly, without a rollup holding them in between. What L1.5 must guarantee For the private settlement case we look at in this post, we want a job to have four properties before we call it L1.5 rather than an operator: - Stateless: once the job is done nobody depends on it, and anyone can take the next one. A worker can keep a cache, as long as it holds nothing the next job needs. - Checked: L1 verifies its output. - Paid without linking: the user can pay for it without revealing who they are. - Landed without an operator: its output reaches L1 without a long-lived account to submit it and pay for it. The last one used to be the hard part, which native account abstraction makes practical. Who sends the transition Under EIP-8141 a transaction is a list of frames. A VERIFY frame can approve execution, payment, or both, and it may use up to 100,000 gas and read only the sender’s own state. So an application contract can check a proof in its own VERIFY frame and pay the fee from the funds it moves. EIP-8250 adds keyed nonces, “for example one derived from a privacy nullifier”, so the chain rejects a double spend the same way it rejects a reused nonce. EIP-8288 lets each mempool node check a proof once, and the block carries “one single recursive STARK” for all of them. With these, only the contract pays for the transaction and any node can relay it, so the user needs no ETH at the address it spends from. Here is a redemption from a privacy pool as we ran it on the Hegota test network (transaction): [0] VERIFY recent roots the pool's root, by slot (EIP-8272) [1] VERIFY the pool checks the proof; approves execution and payment [2] SENDER the pool withdraw: pays the recipient, less the fee [3] DEFAULT the pool refunds the unused fee to the recipient nonce key: the note's nullifier hash (EIP-8250) signatures: none Frame [0] reads a recent root through EIP-8272, and frame [1] is where L1 checks the proof. With EIP-8288, the proof check moves out of this frame into a separate dependency frame. Either way, L1 checks the proof before any funds move. Part 2: L1.5 in context Naming, and prior art This pattern somehow applies at any scale, from one application to an L2 to the protocol itself. Compared with an L2, an L2 holds its users’ state and so its users need an exit, while, on the opposite, L1.5 holds no state. L1.5 is also independent of based and native, which describe who sequences and who executes, while L1.5 is about who holds the state. We call it “1.5” as we refer to its position, which is between the wallet and L1. If we really need to give it an “X-rollup” name, the X would be ephemeral. Several roles on Ethereum, existing or planned, already do part of this. In each of them someone computes while the state stays with the user or on L1, though each has only some of the four properties above: Role What it computes What it keeps afterwards relayer, for Tornado Cash or Railgun submits a withdrawal the user proved, pays its gas for a fee nothing; the contract keeps the tree, the nullifiers and the proof check batch inserter, e.g. World ID’s sequencer Merkle tree updates for a batch, with a proof nothing the contract depends on Privacy Pools’ association-set provider the deposits it vouches for, posted as a root the set’s contents, off chain builder and relay, for MEV-Boost a block for the proposer nothing once the block is out keyper, for an encrypted mempool a key, released after the order is fixed its key share, until rotation includer, for FOCIL a list “according to their subjective view of the mempool” nothing after its slot Reality check: Nobody needs an exit from a relayer or an includer, because if one fails the user picks another. However, two of these roles are not yet open to anyone. Privacy Pools’ contract accepts a root from one role only, and the MEV-Boost relay is “a trusted party” in the words of ePBS EIP. Why now Efficiency was the main obstacle, and it has been getting smaller with each step. Native account abstraction has been proposed since 2020 (EIP-2938). Frame transactions were created in January 2026, replacing EIP-7701. Keyed nonces followed in April, and frame transactions were Scheduled for Inclusion in Hegota in August. The Strawmap places both in Hegota, and EIP-8288’s STARK aggregation in the fork after it. These STARKs are hash-based, and therefore post-quantum, and recursion lets a node check each proof once while the block carries one proof for all of them. The Strawmap covers L1 but says little about what applications should do with these changes, and L1.5 is one answer. Native rollups, the first un-capture An L2 commits to a state in a contract that users deposit into and withdraw from. It has two independent sets of tools, verification (fraud or validity proofs) and compute (ZK, MPC, FHE or a TEE). Whatever the combination, the users’ state stays in the L2’s contract, so every L2 needs an exit. Native rollups were proposed in January 2025 with a similar timing argument: “a big idea whose time may have finally come”. A native rollup verifies its state transitions with L1’s own execution engine, through an EXECUTE precompile, “dramatically simplifying synchronous composability”. The proposal is now EIP-8079, the Strawmap’s headliner for L* (December 2029). Native rollups are mostly seen as a fix for L2 fragmentation, but IMHO they do more. State inside the rollup can be composed with state outside it, which is a first step toward un-capturing state. A user who keeps an ERC-20 on L1 could trade, in one transaction, against a central limit order book kept in the rollup. Native account abstraction goes a step further, since the order book itself can live on L1 as a contract that sends and pays for its own settlement transactions. A matcher in L1.5 proves a batch of matches and any node relays it to the order book, which checks the proof in its VERIFY frame. If the matcher stops, another one takes over. The next generation of Ethereum applications This opens up a new kind of applications, where the wallet keeps the user’s state in the clear, L1 keeps the shared state and a commitment to each user’s state and only verifies, and L1.5 computes and proves. Some applications may get there gradually, starting from a native rollup. Later, the L1.5 part can be an ephemeral layer that is put together on demand. It collects what it needs from L1 and from the users, computes, posts the result to L1 with a proof, and disbands. Below are three directions which we think can be interesting. We only make rough sketches (and some depend on Ethereum upgrades that are only proposed so far). Gas-less payments in privacy-preserving applications (for example, a Stealth Address Protocol for assets other than ETH). Blind gas tickets have been proposed before. Vitalik described aggregators that sell a set of tickets up front, each “encoded using a Chaumian blinding scheme”, and in Toni’s Gas Ticketing a coordinator funds an unfunded address when a ticket is redeemed. In both, users trust a single issuer. With L1.5, a committee issues the tickets with a threshold blind signature, so no single member can sign a ticket alone and none of them sees what it signs, and the tickets are redeemed on L1 through native account abstraction. The user buys tickets from any account and later spends one from a fresh account, and the application’s paymaster checks the ticket in its VERIFY frame. Since the issuers cannot link a ticket to its purchase, the user never needs ETH at the address it uses, and never has to fund that address from one linked to it. Fair exchange for Ethereum services. Suppose a user pays a private RPC with a blind ticket for a PIR query. The server should be paid only if its answer is correct, which a plain payment does not enforce. The user can check an answer against a block header, but a server that takes the ticket and never answers leaves no evidence (the fisherman’s dilemma), and a user who disputes a wrong answer reveals the query. L1.5 can turn this into a fair exchange, similar to zero-knowledge contingent payments for services. The server posts its answer encrypted to the user, with a proof that it is the correct answer to the encrypted query against a recent header’s state root, and the ticket pays out only if that proof verifies in the paymaster’s VERIFY frame. The query stays private and the server is paid only for a correct answer, so there is nothing to dispute. Note that the PIR query does not change the state it reads, and only the verification and the payment settle on L1. A stealth Privacy Pool. A Privacy Pool is visible on chain, since a deposit into a known contract shows that the user used a privacy tool. We would like to find out whether L1.5 can make the pool stealth, so that users never touch a recognizable pool contract. An L1.5 round shuffles many users’ ETH to fresh stealth addresses, and each leg is an ordinary transfer. The chain would then show no pool contract, deposit or withdrawal, only payments between fresh addresses, and each one could be a payment, a swap or part of a shuffle. Compliance can still be offered if wanted, with an association-set provider (ASP) vouching for the funds each participant brings and giving its proof to the round instead of to a contract. What privacy such a round gives overall, and how input-eligibility proofs carry over to it, we leave for later work. The protocol is L1.5 at scale and its implications Looking back and forward, Ethereum’s own protocol already runs short-lived roles over long-lived shared state, at a much larger scale: - Execution: every node re-executes so that no node has to trust another. With zkEVM proofs (the Strawmap’s “gigagas L1”), one party computes and everyone verifies. - Consensus: the validator set is shuffled into new committees every epoch. Each committee lasts an epoch while the stake behind it stays, and committees are checked through their signatures. - Data availability: nodes share the work of serving data, and check it by sampling. - FOCIL and LUCID work like L1.5 roles built into the protocol, with 16 includers per slot whose lists the block must respect, and a key publisher whose timely key release the network checks. We see two lines of work here. One is to build new functions as L1.5, such as tickets, shuffles, fair exchange, proving committees and aggregation. The other is to reuse what the execution, consensus and data availability layers already do: draw committees from a seed fixed in advance (studied as fluid MPC and YOSO), make every member’s actions public and signed, post bonds that are burned on failure, force-include L1.5 outputs as FOCIL does for transactions, and publish and sample whatever must be public. At this point, perhaps one can as well put mempool into the L1.5 class. From “an L2” to “wallet + an L1.5” And perhaps we can even make the canonical version a new standard when the native account abstraction EIPs are more matured. Some L2 applications can move toward this model step by step: - Move owned state to wallets. Keep only commitments and nullifiers on L1, as privacy pools already do, and let wallets hold the openings. - Let the contract send its own transactions. Check the proof in the contract’s VERIFY frame, pay the fee from the funds being moved, and use the nullifier as the nonce key. No sequencer or relayer is needed. - Make proving and submitting open jobs. The user’s device can prove, and stronger nodes can help on public statement, composed in a Lego style, and any node can relay. Moving state into the wallet also moves responsibility to the wallet: - One recoverable seed. Derive every secret from one seed. Make it recoverable through guardians plus a phrase the user keeps, with a delay the user can cancel. - Prove on the device. If a committee must help, give it secret shares (co-SNARK), never the full witness. Proofs can also be composed Lego-style and aggregated. - Pay blindly (sketch). Buy tickets from one account and spend them from fresh ones. Never fund a fresh address from a known one, and never sweep fresh addresses into one. Visit Topic to respond. You are receiving this because you enabled mailing list mode. Tornado Cash: tornadocash/tornado-core Railgun: Railgun-Privacy/contract sequencer: worldcoin/signup-sequencer Privacy Pools: 0xbow-io/privacy-pools-core MEV-Boost: flashbots/mev-boost fisherman’s dilemma: github.com/ethereum/research/wiki/A-note-on-data-…

[ethresear.ch] [Networking] Inventory of PQ P2P Migrations in the Consensus Layer adust09 October 27 Author: @adust09 from Nyx Foundation Abstract In this post, we will take stock of the challenges facing PQ P2P in the consensus layer. Ethereum consensus-layer networking has no adopted post-quantum migration profile. Replacing validator BLS signatures with leanXMSS does not update the networking identities and handshakes used by ENRs, Discovery v5, libp2p Peer IDs, or QUIC/TLS. The migration has three linked targets: - Discovery: ENR signatures, Discovery identity proofs, and Discovery key exchange. - Connection key exchange: TLS 1.3 key agreement inside QUIC. - Connection authentication: libp2p TLS identity binding and TLS CertificateVerify. The main constraints are structural: an ENR is limited to 300 bytes, a Discovery packet to 1,280 bytes, and hybrid key exchange does not provide PQ authentication. In practice, hash-based signatures are being promoted for consensus signatures, but the size limits of the P2P layer make lattice-based schemes the de facto standard candidates for networking. This inventory maps the required changes without selecting an algorithm, encoding, or activation schedule. This article is intended for developers working on the network layer and libp2p. Please feel free to send me your feedback. 1. Scope This post covers Ethereum CL networking over libp2p and QUIC: Discovery v5 + ENR ↓ client discovery adapter ENR → multiaddrs + expected Peer ID ↓ QUIC + TLS 1.3 ↓ libp2p streams ↓ gossipsub and request/response protocols The Execution Layer and TCP/Noise fallback are outside the handshake analysis. They still need compatible migration work: the current consensus-specification development branch requires both transports and treats QUIC as primary. QUIC-only scope is therefore an analytical boundary, not a deployment proposal. This post does not select a PQ signature, KEM, fork, or rollout date. 2. Current discovery-to-message path First, let’s take a look at the current spec. Discovery and libp2p use separate sessions and keys. The current CL profile derives the Discovery node ID and libp2p Peer ID from one secp256k1 networking key, but the identifiers are not interchangeable: the node ID selects records in the Discovery routing table, while the Peer ID identifies the libp2p endpoint. Figure 1. The node ID is Ethereum’s. The Peer ID is libp2p’s. A node starts from bootnode or cached ENRs. Discovery v5 performs Kademlia-style lookups with FINDNODE and NODES, then returns authenticated records. The client adapter converts a selected ENR into dialable multiaddrs and the expected Peer ID. Figure 2. Discovery returns an ENR, then the client dials its QUIC endpoint and checks the Peer ID. QUIC establishes a new TLS 1.3 session; Discovery keys and transcripts are not reused. The client checks the authenticated libp2p identity against the Peer ID derived from the ENR. The client then performs Ethereum’s Status exchange to check fork and checkpoint compatibility before normal traffic begins. Figure 3. Discovery and QUIC/libp2p are separate authenticated stages. Lighthouse, Prysm, Teku, Nimbus, Lodestar, and Grandine bind both systems to one secp256k1 key. If future designs separate them, the node-ID-to-Peer-ID mapping must be authenticated and normative; client-local conventions would create identity-substitution and interoperability risks. 3. Cryptographic inventory As we saw in Chapter 2, some cryptographic primitives need to be replaced. Component Role Current scheme Quantum-relevant threat ENR Discovery record signature secp256k1 ECDSA Forge records after quantum capability exists Discovery v5 Session key exchange secp256k1 ECDH Record traffic now and decrypt it later Discovery v5 Handshake identity proof secp256k1 ECDSA Impersonate nodes and forge handshakes libp2p TLS extension Peer identity–certificate binding secp256k1 ECDSA in the CL profile Impersonate a Peer ID QUIC/TLS 1.3 Session key exchange Negotiated DHE/ECDHE Record traffic now and decrypt it later TLS 1.3 CertificateVerify Certificate-key signature Forge the secure-channel handshake The threats have different timelines: - Key exchange: recorded ciphertext can be decrypted when the classical agreement is broken. - Signatures: the attacker needs quantum capability at the time of impersonation or forgery. Hybrid key exchange can therefore precede a complete PQ identity design, but it is not a complete P2P migration. 4. Post-quantum migration for Discovery Here, let’s review the challenges related to the replacement targets. First up is the one concerning Discv5. 4.1 ENR format and PQ size constraints An ENR is an RLP list of at most 300 bytes: [signature, seq, k₁, v₁, k₂, v₂, ...] For the v4 identity scheme, the 64-byte secp256k1 signature covers: keccak256(RLP([seq, k₁, v₁, k₂, v₂, ...])) The signed fields include the identity key and advertised endpoints. udp and quic identify separate listening ports. Figure 4. The v4 signature covers the RLP-encoded content, not the signature itself. The size limits rule out direct substitution with common PQ signatures: Item Size Maximum complete ENR 300 bytes Maximum Discovery v5 packet 1,280 bytes Current secp256k1 ENR signature 64 bytes Current compressed secp256k1 public key 33 bytes ML-DSA-44 public key 1,312 bytes ML-DSA-44 signature 2,420 bytes ML-DSA-44 is an example, not a selection. Its public key already exceeds both limits, and its signature is larger still. Since the identity key, signature, endpoints, and metadata share the ENR budget, PQ migration requires a new record format or credential-distribution model. Other schemes make different size trade-offs, but none should be assumed to be a drop-in replacement. Scheme families diverge by layer. Ethereum’s consensus-signature work promotes hash-based schemes such as XMSS and SLH-DSA, which offer high confidence but carry signatures of several kilobytes or more. The P2P layer cannot afford that overhead inside a 300-byte ENR, so standardized lattice-based schemes such as ML-DSA dominate practical candidates for networking. This describes the community’s current tendency, not a selection. 4.2 Discovery v5 session authentication and migration challenges On first contact, the initiator knows the recipient’s ENR but has no session keys: - The initiator sends an ordinary packet with random message content. - The recipient replies with a WHOAREYOU challenge containing an identity nonce and ENR sequence. - The initiator sends an identity signature, ephemeral key, optional ENR, and an encrypted request such as FINDNODE. - The recipient verifies the proof, derives keys, and returns an encrypted response such as NODES. - Both sides reuse the session keys until expiry. Discovery derives AES-128-GCM keys from secp256k1 ECDH and HKDF-SHA-256. ECDSA authenticates the handshake; ECDH alone does not. Figure 5. Discovery and libp2p perform separate key exchanges. PQ migration must replace both the ECDSA identity proof and ECDH while preserving the binding among the ENR, node ID, endpoints, and Peer ID. A hybrid KEM protects the session secret but does not authenticate the peer. PQ authentication must either fit within the 1,280-byte packet budget or use separately authenticated credentials. Post-quantum Discovery therefore needs common rules for: - proving that the ENR, node ID, Peer ID, and advertised endpoints belong to the same node; - deciding where large PQ public keys and signatures are stored and how they are retrieved, cached, and refreshed; - operating the current v4 scheme alongside its successor without allowing downgrade attacks; - limiting oversized Discovery packets and expensive Discovery-side cryptography (decapsulation and signature verification) to resist denial-of-service attacks; - defining one encoding, error behavior, and set of test vectors that every client implements. 5. Post-quantum migration for connection key exchange Let’s look at key exchange. From this point on, support for libp2p is required. QUIC uses TLS 1.3. A classical ECDHE secret feeds the TLS key schedule; a hybrid group adds an ML-KEM secret. TLS 1.3 key share Client share Server share Property added X25519 32 bytes 32 bytes Classical forward secrecy X25519MLKEM768 1,216 bytes 1,120 bytes Classical + ML-KEM hybrid secrecy RFC 10024 standardizes hybrid TLS 1.3 groups. Ethereum clients still need: - a common TLS profile and compatible libraries; - QUIC handshake-size, latency, CPU, and memory measurements; - deterministic negotiation and downgrade-safe fallback rules; - cross-client tests and telemetry for configured, negotiated, and failed hybrid sessions. Hybrid secrecy protects key establishment; it does not replace the signatures used for connection authentication. 6. Post-quantum migration for connection authentication Next up is authentication. The libp2p TLS handshake has two signing roles: - Peer-identity binding: the long-term libp2p key signs the TLS certificate public key, binding the channel to the expected Peer ID. - TLS CertificateVerify: the certificate key signs the TLS transcript, proving possession of that key. PQ key exchange changes neither signature. Both need a PQ or hybrid plan. Signature role Open algorithm question Required continuity and tests Peer-identity binding PQ-only or hybrid? Peer ID derivation, identity binding, rotation, revocation, expected-peer checks TLS CertificateVerify PQ-only or hybrid? TLS library support, encoding, transcript compatibility, cross-client negotiation 7. Prior work and unresolved areas Several studies have already been conducted. - The post-quantum task list separates node identity, ENRs, discovery, handshakes, encryption, and bootnodes, but does not define a CL interoperability profile. - Towards a Quantum-Safe P2P for Ethereum quantifies PQ size growth and shows why discovery needs redesign rather than a field-for-field algorithm swap. - The signature-free post-quantum RLPx handshake studies static KEM identity and delayed authentication for the Execution Layer Discv4/RLPx path, not CL Discovery v5/libp2p. On the standards side, NIST has finalized ML-KEM (FIPS 203), ML-DSA (FIPS 204), and SLH-DSA (FIPS 205), with FN-DSA still in draft (FIPS 206). The IETF has standardized TLS 1.3 (RFC 8446) and hybrid PQ/T key exchange for TLS 1.3 (RFC 10024); hash-based XMSS (RFC 8391) and LMS (RFC 8554) are standardized separately. In libp2p, ML-DSA peer identities and PKIX/PKCS#8 key encodings remain open proposals. No standard defines the Ethereum CL P2P profile this document calls for. Migration challenge summary Ethereum CL P2P migration requires coordinated changes to three boundaries: - Discovery needs new identity, record, and handshake formats. - QUIC/TLS needs downgrade-safe hybrid key exchange. - libp2p/TLS needs PQ plans for both identity binding and CertificateVerify. At this point, there are no specific plans in place. It would be preferable for the Ethereum team to take the lead on planning Discv5, while the libp2p team takes the lead on everything else. The overall migration cannot be completed without cooperation from the client teams. Next, I plan to post a specific migration plan focused on Discv5. Visit Topic to respond. You are receiving this because you enabled mailing list mode. ENRs: github.com/ethereum/devp2p/blob/2c19a28b25c294877… Discovery v5: github.com/ethereum/devp2p/tree/master/discv5 libp2p TLS: github.com/libp2p/specs/blob/c750236de43cd8b246a8… ML-DSA peer identities: specs#710 PKIX/PKCS#8 key encodings: specs#711

[ethresear.ch] [Security] Lean verification of EIP-7002: system-call success and FIFO requests skbaek October 26 Since Prague, execution-layer requests for validator exits and partial withdrawals go through a 504-byte contract at 0x00000961Ef480Eb55e80D19ad83579A64c007002, hand-written for the geas assembler. At the end of every block the protocol makes a system call to it, and that call is consensus-critical: EIP-7002 requires a block whose call fails to be invalidated. We proved two properties of the deployed runtime bytes in Lean 4: - The system call always succeeds, whatever the contract’s storage holds, and uses at most 210,000 of the 30,000,000 gas it is given. - Requests leave in exactly the order they arrived. Over any valid history since the contract’s deployment, the committed submissions are exactly the emitted withdrawal requests followed by the entries still queued. Both are stated against Jaune, an executable semantics of the EVM and block processing, also written in Lean, and cover the Prague, Osaka, BPO1 and BPO2 forks. The proofs use no axioms beyond Lean’s standard three: propext, Classical.choice and Quot.sound. Before deployment, the contract had already been examined by four audits and a loop-bounded Halmos check. The results here connect the deployed bytes to Jaune’s block processing, with exact gas, and follow requests from submission to delivery across histories. The system call succeeds The statement is short enough to quote. It has no premise about storage: theorem checked_system_totality {benv : Benv} (fork : CoveredFork benv.stat.fork) (installed : benv.state.getCode withdrawalRequestPredeployAddress = Blanc.withdrawalRequestCode) : processCheckedSystemTransaction benv withdrawalRequestPredeployAddress [] = .ok ((systemProtocolPost benv).state, systemProtocolOutput benv) ∧ (systemProtocolOutput benv).gasLeft = systemTransactionGas - systemProtocolGas benv ∧ systemProtocolGas benv ≤ 210000 Here processCheckedSystemTransaction is the checked system-call routine that Jaune’s block processing uses. It returns .ok only when the call ends without error; otherwise it rejects the block. So under a covered fork, with the canonical code installed, the call succeeds. Its gas cost systemProtocolGas benv is computed exactly from the state and never exceeds 210,000. (checked_system_totality) A companion theorem shows that valid histories under the covered forks keep the canonical code installed. (history_canonical_code) Requests are first in, first out The FIFO theorem, history_fifo, concludes HistoryFifo history: def HistoryFifo {cfg : ChainConfig} {checkpoint final : BlockChain} (history : ConfiguredHistoryTrace cfg checkpoint final) : Prop := submissions history = emissions history ++ remainingQueue history Each of the three lists is read directly off the execution history: - submissions lists every committed submission call to the contract, including calls made from inside transactions, with its caller and calldata. A submission is committed if it succeeds and no enclosing call rolls it back. - emissions lists the withdrawal requests (request type 1) that the blocks actually output, in block order and in order within each block. - remainingQueue reads the live queue from the contract’s final storage, from the stored head pointer up to the stored tail. All three produce records in the same 76-byte format (caller, public key, amount), so equality compares every field. Because the equation compares lists, it respects order and multiplicity: the same request submitted twice counts twice. And because it holds for every valid history, it holds after every block, starting from the empty history. So no committed submission is ever lost, duplicated, reordered, or emitted before it was submitted. Two further results describe how the queue is served: - Service rule. Each block emits the first min(16, queue length) entries, and every committed submission paid at least the fee the bytecode computes. (That fee is not always the EIP’s; see The fee below.) (block_word_fifo) - Delivery bound. Suppose an entry is at zero-based position q in the queue when block B computes its requests. Then it is emitted exactly \lfloor q/16 \rfloor blocks after B (in B itself if q < 16), and later submissions cannot delay it. This holds in any extension of the history that runs that long and still meets the premises; it does not claim that the chain will produce those blocks. (block_word_delivery_from_deployment) What the FIFO theorem assumes Every history is valid under Jaune’s configured block processing. Each block also satisfies a balance bound: all execution-layer balances before the block, plus the block’s incoming consensus-layer withdrawal credits, sum to less than 2^{256} wei. There is no hash premise. The remaining premises fall into three groups. Several concern the system address 0xfffffffffffffffffffffffffffffffffffffffe (0xff…fe below), which the protocol uses as the caller of its system calls. - Deployment. The history begins with the contract’s own deployment: a Cancun block containing the canonical CREATE transaction, with the canonical creation code, zero value, enough gas and no address collision. The rest of that block, and every block until activation, runs Cancun. In that stretch none of the blocks’ transactions is sent from the system address (the protocol’s own system calls are not transactions, so they are unaffected) and no contract creation runs at it, even one that reverts. The system address has no code right after the deployment transaction, and each later block starts with the canonical EIP-4788 beacon-roots code already in place. - After activation. Every block runs Prague, Osaka, BPO1 or BPO2 under the same valid chain configuration. At activation, the other three system contracts (EIP-2935, EIP-4788 and EIP-7251) hold their canonical code. Throughout, no block transaction is sent from the system address, no EIP-7702 authorization is signed by it, and no contract creation runs at it, even one that reverts. - Capacity. There are at most 2^{254} committed submissions after activation. This bound only keeps counters and queue addresses from wrapping in 256-bit arithmetic during the proof; the contract enforces no such limit. The contract’s starting state is not assumed. A deployment bridge proves it: at activation the contract holds its canonical runtime and its post-deployment storage (an empty queue; count, head and tail zero; and excess 2^{256}-1, the inhibitor value that blocks submissions until the first system call). It also proves that no submissions were committed before activation: Cancun makes no system call to the contract, so the excess stays at the inhibitor, and every call from any other caller reverts. The one starting fact it does not derive is that the system address has no code. Deployment cannot establish that, so it is assumed right after deployment and carried forward to activation. That condition is not a formality. A machine-checked counterexample puts code at the system address; a user transaction triggers that code, which then calls EIP-7002. EIP-7002 recognises the system call only by its caller, so it treats this call as the system call and drains the queue before the block’s real one. The counterexample meets every other premise of the earlier form of the theorem, which started from an assumed post-deployment state rather than from deployment. So the condition cannot be dropped from that earlier theorem. The counterexample does not start from a canonical deployment, though, and it does not show that mainnet can reach such a state. The theorem is about execution histories; it does not authenticate any mainnet transaction or state root. For the earlier form, the verification package of a related paper (see below) records what three RPC providers reported at block 22,431,083, the last before Prague: EIP-7002’s storage was still in its post-deployment state, with an empty queue and the excess at the inhibitor; each of the four system contracts (EIP-2935, EIP-4788, EIP-7002 and EIP-7251) held its canonical code; the system address held no code. These observations match the earlier form’s starting premises but are not authenticated state proofs. Applying either form to mainnet also depends on Jaune’s fidelity to Ethereum, which fixture tests support but these proofs do not establish. The fee The EIP specifies fake_exponential over unbounded integers. The bytecode computes it in 256-bit words, which can overflow. Two pre-deployment audits flagged this: Blackthorn L-8 and Sigma Prime PEC-03. We proved that the bytecode’s fee never exceeds the EIP’s, and that the two are equal exactly when no intermediate value of the calculation wraps. The gap can be exercised. A machine-checked three-block history meets the premises of the earlier form of the FIFO theorem, yet commits a submission that paid less than the EIP’s fee. So a guarantee that every submission paid the EIP fee would be false, which is why the FIFO results refer to the fee the bytecode computes. This history, however, does not start from a canonical deployment, similar to the drain counterexample. It is also far from mainnet. The witness runs a synthetic Prague chain and reaches an excess of 2,893 with 2,895 submissions in one block, whose gas limit is 2^{29}. Each pays only 1 wei, because a block’s fee is set by the excess left by the previous block, here zero; the excess then rises by the number of submissions above the target of two. The underpaying submission, in the next block, pays 2^{245} wei, about 5.65\times10^{55} ETH, from an initial allocation vastly larger than mainnet’s entire supply. It refutes the universal fee guarantee; it does not show that such an underpayment can happen on mainnet. By direct computation, outside the proofs, the two fees agree at every excess up to 2,892. For scale, the related paper’s verification package records a mainnet excess of 666 on 19 December 2025. Sigma Prime noted that optimisations or a higher block gas limit might make the overflow threshold reachable. Reaching the threshold would not be enough, though: at excess 2,893 even the bytecode’s lower fee is about 3.2\times10^{55} ETH, so no real account could pay it. What this does not say - Nothing about Amsterdam or later forks. The results cover only blocks that run Cancun before activation and the four covered forks after it. - Nothing about how the consensus layer processes the requests, including whether the caller is entitled to act on the validator or when a requested exit or withdrawal completes. - Nothing about whether the fee parameters are economically sound, or about storage growth. Dequeued slots stay in storage. - No transaction-level liveness theorem. There are frame-level ones: once the inhibitor is cleared, a submission from any caller other than the system address succeeds at an exact cost if it pays at least the EIP’s fee, carries 56 bytes of input, is not static, and has more than 2,300 gas beyond its cost. Fee equality is not required, since paying the EIP’s fee also covers the bytecode’s. This says nothing about whether the transaction is admitted or included. - No corresponding totality or FIFO theorem for the EIP-7251 contract. Evidence and artifacts Every Lean result above is at one source revision: Blanc 7954405c, with Jaune ff22ec80, using Lean v4.35.0. Besides the theorems linked above, it contains the frame-level submission liveness theorem. The pinned Jaune’s README reports its strict current-mainnet fixture lane over the execution-specs release tests@v21.0.1: all 4,968 files of its manifest pass, with no expected-failure allowance. That is a result for that source and fixture snapshot, not a claim about all Ethereum execution behavior. The axiom audit walks dependencies from scratch. It does not rely on #print axioms, whose imported-inductive reporting bug affects the completeness of the report, though not kernel soundness. The audit bounds the axioms used, but it cannot show that the statements capture the intended protocol properties. A related paper, arXiv:2610.19764v1, covers this contract (§4.5 and Appendix F.5) among eight deployed artifacts; this post covers only EIP-7002, because its failure invalidates a block. The paper is based on an older snapshot of the corpus: Blanc 5048a51f with Jaune 2737c8eb, using Lean v4.34.0. The FIFO theorem here is newer than the paper’s, which started from an assumed post-deployment state rather than from deployment. Its verification package, Zenodo DOI 10.5281/zenodo.23351349, records that snapshot’s checks, including a leanchecker replay and the mainnet observations cited above. AI agents wrote the proofs and statements under my direction and helped draft this post. Corrections are welcome, especially on the definitions of the three lists in the FIFO equation, the assumptions and the connection to mainnet. Questions - Is there a route to code or a transaction at the system address that the premises miss? - For future forks, which system contracts or properties would be most valuable to verify before their bytecode is finalized for deployment, and what evidence would client teams need to use those results? - For those following the client FV thread and the client TCB thread: Jaune is an executable EL semantics in Lean, with the fixture coverage above, and the results here carry over to mainnet only insofar as Jaune agrees with the clients. Where might it diverge from them, and which behaviours would you test first to find out? Visit Topic to respond. You are receiving this because you enabled mailing list mode. four audits: github.com/ethereum/audits/tree/master/Pectra loop-bounded Halmos check: daejunpark/sys-asm-halmos processCheckedSystemTransaction: github.com/skbaek/jaune/blob/ff22ec809b7431cc8397… checked_system_totality: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… history_canonical_code: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… history_fifo: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… HistoryFifo history: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… submissions: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… emissions: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… remainingQueue: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… block_word_fifo: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… block_word_delivery_from_deployment: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… deployment bridge: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… machine-checked counterexample: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… Blackthorn L-8: github.com/ethereum/audits/blob/f4a9ecad63727076a… Sigma Prime PEC-03: github.com/ethereum/audits/blob/f4a9ecad63727076a… proved: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… machine-checked three-block history: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… Blanc 7954405c: github.com/skbaek/blanc/tree/7954405cba63d64a3a4d… Jaune ff22ec80: github.com/skbaek/jaune/tree/ff22ec809b7431cc8397… submission liveness: github.com/skbaek/blanc/blob/7954405cba63d64a3a4d… README: github.com/skbaek/jaune/blob/ff22ec809b7431cc8397… imported-inductive reporting bug: lean4#15226 Blanc 5048a51f: github.com/skbaek/blanc/tree/5048a51f Jaune 2737c8eb: github.com/skbaek/jaune/tree/2737c8eb

This weekend we launched EthLib, a Lean4 library for Ethereum! The goal is to bring Ethereum's primitives, specifications and theorems into one place, building a shared foundation for formally specifying and proving things about Ethereum. ethereum/EthLib

Keycard Pal 1.15.0: ERC-7730 clear signing in an air-gapped Keycard app Keycard Pal is an open-source (MIT) Android and iOS app that works as an air-gapped signer with your Keycard. Your software wallet shows a QR code, Keycard Pal shows what you are about to sign, and the Keycard signs it with a tap. 1.15.0 adds clear signing. Instead of a function selector and raw arguments, the review says what a contract call or EIP-712 message does ("Stake ETH", "Repay loan", "Authorize spending of token") and labels every field: amounts with their token, addresses checksummed, dates readable. How it works - The descriptions come from the ERC-7730 clear-signing registry (github.com/ethereum/clear-signing-erc7730-registry). A snapshot ships in the app, so it works without a network. The Offline build has no internet permission at all. - A description is used only when the chain, contract and function (or the EIP-712 domain and type) match. Otherwise the app falls back to its own decoding. - Each review says whether an auditor reviewed the description, from the ERC-8176 attestations in the registry (Cyfrin, for now). Unreviewed descriptions still show, marked "Not reviewed by an auditor". - Settings can import a newer registry zip. The online build can also download one; that is off until you turn it on. Dapps to try it with: Uniswap (Permit2, UniswapX orders), 1inch, ParaSwap, KyberSwap and LI.FI swaps, Aave, Morpho, Lido, Safe, WETH, USDC transfer authorizations, and 60+ other projects in the registry. What it can't do: where a description expects a name the app cannot know offline, such as an address book entry or an NFT collection name, you see the checksummed address or the token ID instead. Get it - Android: Google Play, GitHub releases or our F-Droid repo, all linked from keycardpal.com. Release APKs are reproducible. - iOS: coming soon. Source and issues: mmlado/keycard-pal. Feedback welcome. How it is built Keycard Pal is developed with substantial help from AI coding assistants (Claude and Codex). I decide what gets built, read and test what goes in, and maintain it myself. What keeps that honest is in the repository: a Jest suite of about 3,150 tests that runs on every pull request, 16 architecture decision records explaining why things are the way they are, a check that the offline build carries no online code, and release APKs that anyone can rebuild byte for byte. Fixes that belonged upstream were sent upstream, to keycard-sdk and to the React Native Keycard bridge. Every release is tested on real Keycards and real phones before it ships.

account abstraction, frameworks, gas reduction, faster transactions, transaction flow conditions, validator operations, AI integration, and more… ethereum/EIPs eips.ethereum.org

EIP stands for Ethereum Improvement Proposal. Ethereum has a long history of development and refinement; each update has been carefully crafted and selected to improve the system while safeguarding user privacy and assets. This work takes time