ethereum

[ethresear.ch] [Execution Layer Research] How large can EIP-8141's validation budget be? A mempool DoS benchmark deanstef November 6 How large can EIP-8141’s validation budget be? A mempool DoS benchmark Authors: Stefano De Angelis, Daniil Ankushin, Manuel Arto. All at Nethermind. Thanks to Thomas for feedback and comments on the initial benchmarking plan. TL;DR - EIP-8141 caps unpaid validation at MAX_VERIFY_GAS = 100k; too low for a Groth16 privacy transfer or post-quantum signatures. - Raising the cap is a DoS risk, since validation and block processing share the node’s CPU. An attacker can send transactions that use the whole cap and then fail, taking CPU from block processing for free. - We tested this risk on a Nethermind node, flooding it with such transactions at caps from 100k to 500k, on one CPU core (the worst case) and three machines. - Without in-client protections, block processing on our slowest machine stays within a 25 ms delay budget only up to 15M gas/s. With Nethermind allowing up to about 100 failing tx/s per connection, that limits the cap to the current 100k. - We show that a MAX_VERIFY_GAS = 300k is viable with an in-client protection that pauses transaction validation while the node processes a block. At 100 tx/s (30M gas/s), block processing then stays within 50 ms, even on p90 mainnet blocks. - The cost moves to the mempool, which admits only 12–27% of honest frame transactions under the flood. 1. Introduction In an ordinary Ethereum transaction the signature check is cheap and fixed. In an EIP-8141 frame transaction the check is arbitrary EVM code in a VERIFY frame. Before admitting the transaction to its mempool, a node simulates its validation prefix, the frames up to and including the first one that sets who pays. The node must run that code to learn whether the transaction is valid, and if the check fails, nobody pays for that work. This opens a denial-of-service (DoS) vector. An attacker sends transactions whose VERIFY frame burns significant CPU and then fails, so the sender pays nothing. As a protection against this risk, EIP-8141 bounds the work with the MAX_VERIFY_GAS parameter, currently set at 100,000 gas per transaction. However, a 100k validation budget admits limited use cases. For example, a privacy transaction with a single-note Groth16 spend needs at least 211,828 gas even after every optimization. Post-quantum accounts hit the same limit as verifying hash-based SPHINCS+ variants in the EVM costs up to 276k gas. Hence, raising that budget is a requirement to make privacy, post-quantum signatures and other relevant use cases practical with frames. This leads to the critical research question for this post: Can the block processing of a node be slowed down with DoS campaigns when the frame validation cap goes up? To answer this question, we ran a DoS campaign against a Nethermind client with EIP-8141 activated. We set the frame validation budget at caps from 100,000 to 500,000, and tested input loads with two types executed in the VERIFY frame: (i) EVM hashing loops and (ii) stuffed secp256k1 signatures. We evaluated the impact on block processing through three metrics: (i) block import delay, (ii) block building delay, and (iii) share of honest transactions admitted. We ran the tests across different hardware tiers covering local builder profiles and our slowest machine. We call an input load safe when the extra time it adds to importing or building a median mainnet block stays within a delay budget of 25 ms. On today’s network that much extra delay makes a node miss the attestation deadline about 0.2 percentage points more often (§3.5). In short, we found the following: - A local builder absorbs about 30M gas/s of validation. Block processing stays within a 25 ms delay budget up to about 30M gas/s of VERIFY work. Each cap reaches that limit at a different transaction rate: 300 tx/s at 100k, 120 at 250k, 100 at 300k and 60 at 500k. At 100 tx/s, 300k is the largest cap within budget. - A full node absorbs only about 15M gas/s. Every node must import each block on time. On our slowest machine, the full-node profile, import stays within 25 ms only up to about 15M gas/s of VERIFY work. At 100 tx/s that is 10M gas/s at 100k but 30M at 300k, so only 100,000 is within budget. - In-client DoS protections unlock 300,000 within budget at 100 tx/s. We implemented protections in the Nethermind client that make mempool validation give way to block import. While the node processes a block, it starts no frame validation of gossiped frame transactions (#13994). Import delay drops to about 2 ms or less on every machine, so a 300,000 cap stays within 25 ms at 100 tx/s. - Honest transaction admission under flood. Failing transactions compete for the same CPU as honest ones. Under a 100 tx/s flood at 300k, the slowest machine admits only 12% of honest frame transactions. 1.1. Why 100k is too low With frames, transactions can adopt different authorization schemes, each with its own verification cost. The table below shows that many of them do not fit under the 100k `MAX_VERIFY_GAS` limit. Scheme Approximate VERIFY gas Source ECDSA 3k (ecrecover), ~7k per signature in a wallet EIP-7951 Safe 3-of-5 multisig ~21k for three signatures, plus overhead EIP-7951 BLS signature 130k to 140k EIP-2537 pricing fflonk verifier ~209k Guo et al. 2024 Groth16 shielded pool ~212k EIP-8141 budget for privacy PLONK verifier ~298k Guo et al. 2024 Hash-based post-quantum (SPHINCS+ variants) 94k to 276k SPHINCS- Lattice post-quantum in pure EVM ~1.2M (ML-DSA-44) to ~4.7M (Falcon-512) Fireblocks ML-DSA-44, Falcon in Solidity 2. Model and definitions 2.1 Threat model We consider an adversary that mounts a DoS attack on a node by sending it transactions that fail validation, with the aim of disrupting its operation. We first define the attack and the transactions it uses. Block-delay attack. The attacker wants to make a node late to import or build blocks, without producing any invalid block. The attacker connects to the node like any peer and writes the VERIFY code of the frame transactions it sends. Since a transaction pays fees only if it passes validation, the attacker crafts transactions that consume the whole validation budget and then fail. Throughout the document we refer to them as failing transactions. Each one names a solvent payer, declares a VERIFY budget equal to the cap C, runs the most CPU-expensive work that budget buys, and fails just before approving payment. The node has spent the CPU, and nobody pays for it. At r failing transactions per second the node runs r × C gas per second of unpaid validation, and that CPU is taken from block processing. The attack succeeds once the delay it adds to processing one block exceeds a delay budget B (§2.2). The attack works at any cap, since at a lower cap the attacker just sends more transactions. Raising the cap still raises the risk, because a node’s defenses limit transactions, not gas. Nethermind, for example, processes about 100 failing transactions per second from one connection (Appendix A), and at that rate a 300k cap delivers three times the load of 100k. The benchmark therefore asks how many failing transactions per second an attacker needs at each cap before r × C exceeds what the node can absorb. 2.2 Notations and metrics Symbol Meaning C The tested VERIFY cap, in gas per transaction. r Failing transactions per second the node processes. f Share of the CPU core the attack takes from block processing (import or build). T Time to process a mainnet block with no attack. Δ(C, r) Block delay, for import or building. B Delay budget. G_B Gas per second of validation a machine absorbs while its block delay stays within B. C_{max(r)} Maximum cap. Load. At rate r and cap C the node runs r × C gas per second of unpaid validation. Metrics. We measure three metrics. - Block-import delay and block-building delay. Δ(C, r) is the time the attack adds to processing one block. We measure it separately for import, which every node does, and for building, which only a proposing node does. It depends on f, the CPU share the attack takes at the load r × C, and on T, the time the block needs without the attack. A block that needs T of CPU gets only 1 − f of the core and takes T / (1 − f), so the attack adds Δ = T · f / (1 − f). For example, if the attack takes 30% of the core, the block gets the remaining 70% and takes T / 0.7 ≈ 1.43 T, so Δ ≈ 0.43 T. - Honest admission. The share of honest frame transactions the node admits to its mempool while under attack. It measures what a node gives up when it limits the CPU spent on validation. We judge the two delays against an acceptable delay budget, set as benchmark parameter B: - Delay budget. B is the largest block delay we accept. - Maximum cap. C_{max(r)} is the largest tested cap whose block delay stays within B at rate r. 3. Methodology 3.1 Hardware We tested the worst case, a node with no spare core to absorb the attack. A single Nethermind node ran on one CPU core, shared by block processing and the validation of failing transactions. We ran it on three machines: Tier Machine CPU Single-thread (PassMark) T, median / p90 block High AMD EPYC 4344P, bare metal, capped at 3.8 GHz Zen 4, 8c/16t ~2,600 27 / 48 ms Mid GCE c2-standard-8 Cascade Lake 3.1 GHz, 4c/8t ~2,300 to 2,400 (est.) 30 / 53 ms Low GCE n1-standard-8 Haswell class 2.3 GHz, 4c/8t ~1,700 (est.) 42 / 74 ms By referencing EIP-7870, High and Mid stand for local builders. Low is the closest we had to a full node (§4.1). 3.2 Load types We built failing transactions from the most CPU-expensive work we found for a validation frame, in two load types: - Keccak-wide. KECCAK256 over 4 KB, repeated N times, then fail. We fixed N so that each transaction consumes nearly the full cap before it fails. - Sig-stuffed. A transaction that verifies many secp256k1 signatures. The verification checks signatures one by one, with the last signature failing, so that the node must process every signature before rejecting the transaction. 3.3 Benchmarks We do not target mainnet blocks directly. Each benchmark repeats a fixed piece of block work (Appendix B), first with no attack and then under a steady load of failing transactions, fixed in gas per second. The attack determines f, how much CPU it takes on hardware. Thus, we apply the same f to mainnet blocks measured at length T (§3.1), and we calculate Δ(C, r) on mainnet values. We ran four benchmarks: - Block building (§4.1). The node builds blocks while it validates a flood of failing transactions, at 5M to 40M gas/s in 5M steps and at every tested cap. - Block import (§4.2). The node imports blocks while it validates a flood of failing transactions, at 5M, 10M, 30M and 50M gas/s and at caps from 250,000 to 400,000. - Honest admission (§5.2). The share of honest frame transactions the node admits under a load of 10M, 30M and 50M gas/s. - Per-connection rate (Appendix A). The node is flooded from one connection at increasing rates, to find how many failing transactions per second one connection gets processed. This is the reference rate r. We report MAX_VERIFY_GAS caps of 100,000 (today’s value), 250,000, 300,000, 400,000 and 500,000. A run is one pass of a benchmark on one machine through every load type, cap and load level. For each load type and cap, the node first processes blocks with no load, which gives the baseline, and then under each load level. Every benchmark ran at least twice on each machine. We report the median over blocks and, where runs differ, the worst run. The benchmark is public in Nethermind #14135. Our runs used the client code at master commit ccb07d17. Block building ran at commit 01cc0069, block import and the per-connection rate (Appendix A) at f859b806, and honest admission at 6de10bc9. Each result can be reproduced at its commit. 3.4 Delay budget We judge the delays against two budgets, B = 25 ms and B = 50 ms. Any ms of delay counts, as a node that imports a block late may miss the attestation deadline, 4 s into the slot. Xatu measures that cost. It records 133 nodes imports over a mainnet block. With no added delay, a node imported the slot’s block only after the deadline in 3.86% of slots. Adding 10 ms of block delay raises that share by 0.07 percentage points, 25 ms by 0.19, 50 ms by 0.39, 100 ms by 0.85 and 250 ms by 2.79. The analysis and its data are public in block-import-delay-budget. There is no threshold below which delay is free, so the budget B is a policy choice. In this work we use 25 ms as the main budget and report 50 ms as a more tolerant one. 4. Benchmark results We now report the two delay benchmarks, block building and block import. 4.1 Block building The table below gives the block-building delay on our three machines. Each cell is the delay added to a median mainnet block with keccak-wide / sig-stuffed load types, at a cap of 300,000. At the same gas per second we obtained the same delay results with the other caps (see Appendix C). A cell marked “≥” means the core was saturated, with f within 0.01 of 0.5. Load High Mid Low 5M gas/s 1.6 / 2.1 ms 1.9 / 2.6 ms 5.0 / 4.6 ms 10M gas/s 3.0 / 4.0 ms 3.6 / 5.1 ms 10.5 / 11.2 ms 15M gas/s 4.7 / 6.4 ms 5.7 / 8.1 ms 18.1 / 17.2 ms 20M gas/s 6.9 / 9.4 ms 7.9 / 12.1 ms 26.1 / 28.6 ms 25M gas/s 8.7 / 12.6 ms 10.3 / 16.2 ms 36.9 / ≥ 42 ms 30M gas/s 11.1 / 17.2 ms 13.2 / 21.5 ms ≥ 42 / ≥ 42 ms 35M gas/s 14.0 / 21.9 ms 17.4 / 28.6 ms ≥ 42 / ≥ 42 ms 40M gas/s 17.0 / ≥ 27 ms 20.2 / ≥ 30 ms ≥ 42 / ≥ 42 ms Once block processing and validation both keep the core busy, the operating system splits it about evenly, so f stops near 0.5 and any excess load queues. The delay is then at least T. The figure below shows f itself, the CPU share the attack takes from building on each machine. Why slower machines suffer more. A slower core needs more of its time to validate the same gas/s, so the attack takes a larger share of it. Below saturation, f is roughly inversely proportional to single-thread performance. At 10M gas/s of sig-stuffed, for example, Low has about two thirds of High’s single-thread rating (1,700 against 2,600) and loses about 1.6 times its share (0.21 against 0.13). Which machine matters. Building delay is judged on High and Mid. Within B = 25 ms both machines hold 30M gas/s for both load types, and 35M within 50 ms. On High and Mid, sig-stuffed is the harder load type, 1.3 to 1.6 times keccak-wide at every load. Low would hold only 15M gas/s within 25 ms and 20M within 50 ms. On the p90 block. A p90 mainnet block takes about 1.8 times as long to process as the median one (§3.1). The delay is proportional to T, so we assume here every delay in the table grows by the same factor. High and Mid then hold 20M gas/s within 25 ms and 30M within 50 ms, and Low 10M and 15M. 4.2 Block import The table below gives the block-import delay on our three machines. Each cell is the delay added to a median mainnet block, keccak-wide / sig-stuffed, at a cap of 300,000. Caps 250,000 and 400,000 give the same delays (Appendix C). Load High Mid Low 5M gas/s 0.8 / 1.3 ms 2.1 / 2.8 ms 4.7 / 5.9 ms 10M gas/s 2.3 / 2.6 ms 3.2 / 5.4 ms 9.8 / 10.9 ms 30M gas/s 9.6 / 15.2 ms 12.3 / 21.9 ms ≥ 42 / ≥ 42 ms 50M gas/s 23.1 / 23.7 ms ≥ 30 / 28.7 ms ≥ 42 / ≥ 42 ms At 50M gas/s every machine is at or near the 0.5 limit. Import loses about the same CPU share as building. Both benchmarks ran at 5M, 10M and 30M gas/s with caps 250,000 to 400,000. Figure below shows that, at the same machine, load type, cap and gas rate, the share f the attack takes from import matches roughly the share it takes from building. On the p90 block. Import delays grow by the same factor of about 1.8. Low then stays within 25 ms only up to 10M gas/s, and within 50 ms up to 15M. 4.3 Input rate per cap The limits above are in gas per second. Since `r` failing transactions per second at cap C deliver r × C gas per second, dividing each machine’s limit by the cap gives the highest transaction rate that cap sustains on the median mainnet block, in tx/s within B = 25 ms / 50 ms: Cap High Mid Low 100,000 350 / 350 300 / 350 150 / 200 250,000 140 / 140 120 / 140 60 / 80 300,000 117 / 117 100 / 117 50 / 67 400,000 88 / 88 75 / 88 38 / 50 500,000 70 / 70 60 / 70 30 / 40 Each value is the worst case over runs and load types, and holds for both building and import, which lose about the same CPU share (§4.2). On High and Mid the 50 ms values are lower bounds, because their core saturates at 40M gas/s, the highest load we measured. The figure below shows the same results for each load type, on the median block. Every cap uses the 300k measurements, which hold for all caps at the same gas per second (Appendix C). 100 tx/s at 300k is 30M gas/s. Assuming 100 tx/s as the reference rate (Appendix A), High and Mid add 11 and 13 ms with keccak-wide failing transactions and 17 and 22 ms with sig-stuffed ones, hence all stay within 25 ms on the median block (§4.1). Low is saturated, at least 42 ms. Along the 100 tx/s line in the figure, High and Mid stay within 25 ms up to 300k with both load types, and up to 400k with keccak-wide. Sig-stuffed exceeds 25 ms at 400k. On the p90 block. At the 100 tx/s reference rate, 300k stays within 25 ms only with keccak-wide failing transactions, 20 ms on High and 23 on Mid. Sig-stuffed ones add 31 and 38 ms, within 50 ms but not 25. 4.4 Discussion We ran the benchmarks in the worst case, with block processing and validation sharing one CPU core, on our High, Mid and Low machines. On each, failing transactions, whose validation prefix burns the whole cap and then fails, delay block processing. We observed that the delay grows with the gas they burn per second as expected. The attack takes about the same CPU share from block import as from block building, and at the same gas/s the cap does not change it. The results therefore answer two questions. - How much validation can be absorbed, in gas/s? On the median mainnet block High absorbs 35M gas/s, Mid 30M and Low 15M. On the p90 block every delay is about 1.8 times larger, and they absorb 25M, 20M and 10M. - How many failing transactions per second an attacker needs to exceed the budget? At MAX_VERIFY_GAS = 100k the attacker needs more than 350, 300 and 150 tx/s on the median block, and more than 250, 200 and 100 on the p90 block. At 300k it needs more than 117, 100 and 50 on the median block, and more than 83, 67 and 33 on the p90 block. At the 100 tx/s reference rate, every machine therefore absorbs MAX_VERIFY_GAS = 100k. At 300k Low exceeds the budget, while High and Mid stay within it on the median block, and on the p90 block only with keccak-wide failing transactions. We note that the operating system splits the core between frames validation and block processing. So the block gets only 1 − f of it and takes longer. As a countermeasure, a client can keep the core for block processing when a block needs it. It can, for example, pause or preempt validation while a block is imported (§5.1), cap the CPU it spends on frame validation per head (§5.2), and downgrade or disconnect a connection whose transactions keep failing validation, which bounds r (Appendix A). None of these was active in our runs above. We implemented them in the Nethermind client and we discuss their effect in the next section. 5. What protections change As part of Nethermind’s frames implementation, we added protections that limit DoS exposure when MAX_VERIFY_GAS increases. 5.1 Block import: pause and preemption We implemented a protection mechanism inside the Nethermind client to prioritize block processing when necessary. With #13994, validation of frame transactions gives way to block processing. No validation prefix starts while a block is processed, and one that is already running is stopped mid-execution. Notably, the interrupted transaction is not rejected but deferred. We ran the import benchmark with and without this protection and measured the delay that failing transactions add to block import. The figure shows the median over runs of the delay on the synthetic import block (Appendix B), which takes 3.3 to 4.2 times as long as a median mainnet block. With sig-stuffed failing transactions at 30M gas/s, the protections remove the 55 ms delay on High, and cut it from 69 to 0.8 ms on Mid and from 173 to 1.9 ms on Low. Due to its limited resources, on Low the protected node validated only about 40% of the transactions sent, so it handled about 12M gas/s rather than 30M and its 1.9 ms must be interpreted as a lower bound. Keccak-wide ones leave at most 2.3 ms on every machine. 5.2 The per-head CPU budget, and honest transactions Nethermind limits the CPU it spends on frame transaction validation per new head with a fixed budget. This is a node policy. Within that budget the node runs the validation prefix of each incoming frame transaction to decide whether to admit it. Failing transactions cannot take more than that budget, so they cannot slow block processing beyond it. But under attack the honest frame transactions, those whose validation prefix succeeds, compete for the same budget. Once failing transactions have spent it, the node defers every honest frame transaction until the next head. In our benchmark we set that budget at 1 s of CPU per head, about 8% of one core over a 12 s slot. Then, alongside the load of failing transactions, we submitted to the node a steady 5 honest frame transactions per second, each with a 50,000 gas validation prefix. The failing transactions were keccak-wide at a cap of 300k. The table below shows the share of these honest transactions the node admitted over three slots, as the median over two runs. Load of failing transactions High Mid Low 10M gas/s (33 tx/s) 86% 81% 37% 30M gas/s (100 tx/s) 27% 25% 12% 50M gas/s (167 tx/s) 14% 13% 1% The figure follows the 12 s between one head and the next, split into four 3s windows. It shows the average share admitted in each window. The × on each curve marks when the budget runs out. On High at 10M gas/s, for example, that happens at 10.6 s. From 6 to 10.6 s the node still admits honest transactions and from 10.6 to 12 s it admits none, so the 6–12 s window averages 73%. At 30M and 50M it runs out at 3.6 and 2.2 s, and on Low at 5.5, 1.9 and 1.2 s. The admitted share in the table is roughly the fraction of those 12 s the budget lasts, except on Low, which is too busy to admit every honest transaction even before the budget runs out. The budget is CPU time, so a slower CPU spends it on fewer transactions, and the loss depends on the load of failing transactions. At MAX_VERIFY_GAS 300k, 100 failing tx/s are 30M gas/s and leave 27% of our honest frame transactions admitted on High and 12% on Low. The budget turns a CPU problem into an inclusion problem, and the trade falls hardest on slower hardware. 6. Picking the number To withstand a flood of 100 failing transactions per second, we identify 300,000 as a safe MAX_VERIFY_GAS, provided block import is protected. With this configuration, we showed that block import stays within a 25 ms delay budget on every machine, and block building on High and Mid. Under flooding, with a per-head CPU budget of about 8% of one core, the node still admits 27% of honest frame transactions on High, 25% on Mid and 12% on Low (§5.2). We measured these shares with keccak-wide failing transactions. The rest of this section shows how that number follows from the measurements, and how it moves with the transaction rate and the delay budget. To pick a number we have to identify the configuration that does not exceed the desired delay budget. Without Nethermind’s protections, the bottleneck is block import on Low, which absorbs 15M gas/s within 25 ms and 20M within 50 ms. With import protected, the bottleneck is block building on High and Mid, which absorb 30M gas/s within 25 ms and 35M gas/s within 50 ms. Writing G_B for the gas per second the bottleneck absorbs within B, the largest cap is: C_{max(r)} = G_B / r, rounded down to a tested cap. For example, with import protected, r = 100 tx/s and B = 25 ms give C_{max} = 30M / 100 = 300,000. The table below gives C_{max} for a few rates, on the median mainnet block with sig-stuffed failing transactions. The first row is the gas per second G_B each setup absorbs within its delay budget B, and every other cell is the largest tested MAX_VERIFY_GAS, in gas per transaction. Failing transactions per second (DoS flood) No protection, B = 25 ms B = 50 ms Import protected, B = 25 ms B = 50 ms G_B (gas/s) 15M 20M 30M 35M 50 tx/s 300,000 400,000 500,000* 500,000* 100 tx/s (reference rate) 100,000* 100,000* 300,000 300,000* 150 tx/s 100,000 100,000* 100,000* 100,000* 200 tx/s < 100,000 100,000 100,000* 100,000* * By the formula the cap is potentially higher than what we tested. For example, High and Mid with protections at 150 tx/s within 50 ms result in ~233k cap, but no cap was tested in our configurations between 100,000 and 250,000. When measured on the p90 block, the configuration with 300,000 at 100 tx/s still holds within the B = 25 ms delay budget for keccak-wide failing transactions only, while for sig-stuffed ones the budget needs to increase to B = 50 ms (§4.3). To conclude, at the 100 tx/s reference rate 300,000 is the largest tested cap that holds on High and Mid, and it admits the use cases that motivate raising the cap, for example privacy transfers with Groth16 proofs and hash-based post-quantum signatures (§1). This result holds only when the execution client protects block import as described in §5.1. Without protections, block import on Low brings the cap back to 100,000 (§4.2). 7. Limits of the study Our benchmarks have the following limitations: - They ran on one client, with a single core shared by block processing and frame validation. - We tested three hardware profiles but none as slow as EIP-7870’s full node tier. - The benchmarks ran on synthetic blocks, not mainnet ones (Appendix B). We measured on them the CPU share f the attack takes, and applied it to the time T for mainnet blocks. This assumes the attack takes the same share from any block work. Appendix B checks it on a much longer block, where it holds within 25% and errs toward overstating the delay, but not on blocks of different content. - Every attack ran with zero state gas. Cold reads from a large existing contract are unmeasured. - Our load counts each failing transaction once, rejected at admission. A frame transaction that is admitted and fails later costs more. It is gossiped to peers that validate it again, which we did not measure. And if it fails VERIFY at build time, it can be re-executed on later builds without paying. Appendix A. Transactions per connection Transactions reach the mempool over the node’s network connections, and Nethermind limits how many it processes from each. Above 600 rejects in 60 s a connection is downgraded and most of its messages ignored. Above 6,000 it is disconnected. The result is that one connection gets at most about 100 failing tx/s processed, which it reaches when it offers about 800 tx/s. Above that it is disconnected. That is the reference rate used throughout this post. The figure shows how many failing transactions per second one connection gets processed, against the rate it offers. A connection offering 50 tx/s is already downgraded, and about 89% of its messages are then ignored, which is why processed throughput climbs so slowly with offered rate. A connection offering 1,000 tx/s or more is disconnected within the 60 s window. The reference rate is a Nethermind DoS-protection policy, not a property of the attack. An attacker holding more connections, or a client that limits a connection less or not at all, delivers a higher rate. The verification load on the node then scales with the cap C and the rate r, as r × C (§4.3). B. The benchmark blocks We ran every benchmark in a test environment, on a single node processing synthetic blocks. While the node built or imported these blocks, a separate stream of failing transactions, the load, reached its mempool, and the node validated them on the same CPU core. Hence, we measured how much of the CPU core the attack takes from block work, the share f (§2.2). Our assumption is that f depends on the machine and on the gas/s load and load type, but not on which block the node is processing. Under that assumption, f measured on a synthetic block carries over to a mainnet block, and the delay follows from the mainnet block time T as Δ = T · f / (1 − f). Below we describe how we estimated f for block building and for block import, and then how we validated the assumption. Block building. The building benchmark repeatedly built a synthetic block holding a single failing transaction of its own, separate from the load. Building it takes about 1 ms of CPU on High at 100k and 3 ms at 300k. If the node completes \text{N}0 builds in a time window without the attack and \text{N} under it, then f = 1 − \text{N} / \text{N}0. Block import. The import benchmark repeatedly imported a synthetic 10M-gas block of keccak-wide hashing. One import takes about 98 ms on High, 98 ms on Mid and 178 ms on Low, about 3.6, 3.3 and 4.2 times a median mainnet block. If one import takes \text{W}0 without the attack and \text{W}0 + Δ under it, then f = Δ / (\text{W}0 + Δ). Validating the assumption. - Different blocks, same f. The two benchmark blocks showed that at the same machine, load type, cap and gas rate they lose the same f within three percentage points of the core on Mid and Low, while on High import loses up to five points less (§4.2). - Synthetic blocks, same f. Our synthetic build takes only 1 to 3 ms, far shorter than a real block. To check that f still holds, we also built a block longer than a p90 mainnet block under the same load. Its delay matched the prediction within 10% in 31 of 36 cases and within 25% in all. - Different caps, same f. At the same gas/s, caps from 100k to 500k take about the same CPU share f, differing by at most 4 percentage points. Hence, we conclude that the CPU consumption follows the load, not the size of each transaction. These checks do not cover block content. A mainnet block mixes storage access, calls and precompiles, and none of our blocks does. C. The delay across caps In §4.1 and §4.2 we set the cap at 300,000. In the figure below we show measurements for different caps, and same input load (gas/s). We notice that what impacts the delay is not the cap itself, but depends on the input load. Block building was run at all five caps and block import at 250,000, 300,000 and 400,000. At the same gas per second, f differs across caps by at most 4 percentage points in both benchmarks, on every machine and load type. The figure shows only building, where the largest gap is on Low with sig-stuffed failing transactions at 5M gas/s. Visit Topic to respond. You are receiving this because you enabled mailing list mode. Daniil Ankushin: github.com/AnkushinDaniil Manuel Arto: github.com/manusw7 tested this risk: nethermind#14135 25 ms delay budget: deanstef/block-import-delay-budget #13994: nethermind#13994 ccb07d17: github.com/NethermindEth/nethermind/commit/ccb07d… 01cc0069: github.com/NethermindEth/nethermind/commit/01cc00… f859b806: github.com/NethermindEth/nethermind/commit/f859b8… 6de10bc9: github.com/NethermindEth/nethermind/commit/6de10b… attestation deadline: github.com/ethereum/consensus-specs/blob/204fb4a1…

[ethresear.ch] [Privacy] A privacy pool on frame transactions: what works, and the case that does not yet AnkushinDaniil November 6 Daniil Ankushin, Nethermind. Verify-budget figures: method by Daniil Ankushin, benchmark and measurements by Manuel Arto. On frame transactions a shielded pool pays its own gas, so a private withdrawal needs no relayer. We ran a real BN254 Groth16 pool this way on current Nethermind master: a withdrawal costs 679,322 gas. With EIP-8250 nonce keys, many withdrawals can come from the one pool address at once. Two things do not work yet. The proof check is over the spec cap on validation gas, and a pool cannot pay for a call from the user’s own address. The pool we ran is soispoke’s minimal-shielded-pool (GitHub - soispoke/minimal-shielded-pool · GitHub). How a withdrawal works In a withdrawal the pool is the sender. Its VERIFY code checks the zk proof and approves execution and payment. The user needs no funded account and does not appear in the transaction. Two drafts make this safe in a public mempool. With EIP-8250 the pool uses the note’s nullifiers as nonce keys. Each withdrawal has its own nonce key, so withdrawals with the pool as sender do not compete for one nonce. A side effect: a nullifier that was already used is a used nonce key, so the protocol refuses a double spend before the pool’s code runs. With EIP-8272 the transaction checks the pool’s Merkle root against a contract of recent roots before the pool’s code runs, so a mempool node never reads the pool’s storage. What it costs All values are from mined receipts on Nethermind master 4bcb9e30, single node. Step Gas Deposit a note, frame tx 990,503 of which state gas 195,840 Deposit a note, plain EIP-1559 call 958,555 Withdrawal, whole transaction 679,322 recent-root VERIFY frame 5,515 pool VERIFY frame (proof check and APPROVE) 405,979 of which execution 210,139 of which state gas for two nullifier keys 195,840 settle SENDER frame 25,526 claim frame 198,338 outside the frames (intrinsic, calldata, key access) 43,964 Bare Groth16 check, as its own transaction, including the 21,000 base 222,991 Transfer, two notes in and two out, whole transaction 1,333,766 of which state gas 293,760 The two nullifier keys cost 195,840 state gas, exactly two times the EIP-8250 price: “each fresh key costs 97920 state gas”. EIP-8250 also charges 12,100 execution gas per key and adds the same amount to the calldata floor. The proof does not fit the shared budget. The validation prefix declares 233,000 execution gas and uses 215,654, over the EIP-8141 cap MAX_VERIFY_GAS. An open change (Update EIP-8141: define MAX_VERIFY_GAS as a shared mempool floor by AnkushinDaniil · Pull Request #12301 · ethereum/EIPs · GitHub) would make that cap a shared mempool floor, with each node free to run higher, and set its value from measurements. Nethermind’s default node budget is already 300,000 (fix(txpool): separate verification floor from node headroom by SIDDHANTCOOKIE · Pull Request #14992 · NethermindEth/nethermind · GitHub), so a default node admitted our withdrawal; a node at the floor would not. The published measurement note (Sizing MAX_VERIFY_GAS: how much unpaid work a node can absorb - HackMD) measured Nethermind d804d33b on an AMD EPYC 4344P and a GCE c2-standard-8, the two local builder machines. There a 300,000 budget held one attacker peer on Nethermind at 100 failing transactions per second when block building may slow by 25 ms, and at 117 at 50 ms. We re-ran the same suites on current Nethermind master (1f6469e64ee) on one shared 12 vCPU AMD EPYC 9645 host. There a 250,000 budget holds one attacker peer on Nethermind at 25 ms with no margin (100 failing transactions per second, against about 100 that one peer gets processed). A 300,000 budget holds 83 at 25 ms, so it holds one peer only at 50 ms (117). The about 100 per peer comes from Nethermind’s flood controller; other clients bound a peer less. Both comparisons cross machines, so these runs cannot tell whether the change comes from the code or the machine. Our 233,000 fits under both. For a pool to work on every node, either the floor rises from measurement, or proof checks leave the per-node budget, for example through proof aggregation. New storage is a large part of the cost. In the withdrawal, state gas is 379,440 of 679,322: 195,840 for the two nullifier keys and 183,600 in the claim frame. Double spends We sent a second withdrawal with the same nullifier keys and a new body. The node refused it at admission: “keyed nonce sequence not current”. When we forced it into a block through the builder, the block included zero transactions. After the first withdrawal, both nullifier slots in the nonce manager read 1. The open question: a pool that only pays Above, the call comes from the pool. Often the user wants to act from their own address while the pool pays the gas out of a note. Here EIP-8250 stops helping. It stores each key under (sender, key). With the user as sender, the same nullifier sent from two addresses is two different keys, and the pool gets no spent-once mark from the protocol. The pool cannot use its own storage instead. Under the EIP-8141 public mempool rules, “SLOAD can be used only to access tx.sender storage”, and here the pool is not the sender. The same rules allow MAX_PENDING_TXS_USING_NON_CANONICAL_PAYMASTER = 1 pending transaction per non-canonical paymaster, so a pool that only pays serves one user at a time on each node. jstinhw raised the case in the MATCHA thread (Mempool Account Transaction Capacity from Historical Activity (MATCHA)): 100 transactions from 100 senders, each with a valid proof for the same note. mmjahanara’s reply in the same thread reaches the same conclusion. We proposed a spec change for this: let a transaction place its keys under the account that approves payment (Update EIP-8250: let a transaction scope its nonce keys to the payer by AnkushinDaniil · Pull Request #12422 · ethereum/EIPs · GitHub). nerolation, an author of EIP-8250, answered: I’m wondering whether improving that app-level nullifier tracking is worth adding a new field and weakening the invariant that all transaction nonces belong to tx.sender. My feeling is no and we may not need the 2d nonces for payers when tx.sender != payer. We closed the PR. The invariant is worth more than one saved transaction. We also tried this shape on master with the unchanged pool: the user’s account approves execution, and the pool’s VERIFY frame approves payment. The node refused it at admission: “frame transaction validation-prefix simulation failed, validation prefix frame reverted”. The pool’s VERIFY code assumes the pool is the sender, so this refusal says nothing about the spec. So today two shapes work in the public mempool: the pool is the sender, as measured above, or two transactions, where the user withdraws to an address that then pays for itself. The third shape stays open: a pool that pays for a call from the user’s own address, in one transaction, through the public mempool. We see no way with the current drafts and have no gas number for it. How to reproduce Nethermind master 4bcb9e30986a86061fc8b7efe33abeeaa31f745a, one node, EIP-8141, EIP-8250, EIP-8272 and EIP-7906 active from block 1. Genesis holds the EIP-8272 recent-root code and the EIP-8250 nonce manager code. Pool: GitHub - soispoke/minimal-shielded-pool · GitHub at bb45b3b9, with the recent-root contract address and the fee parameter index updated to the current specs. Proofs come from the repository’s own tooling. Visit Topic to respond. You are receiving this because you enabled mailing list mode. GitHub - soispoke/minimal-shielded-pool · GitHub: soispoke/minimal-shielded-pool Update EIP-8141: define MAX_VERIFY_GAS as a shared mempool floor by AnkushinDaniil · Pull Request #12301 · ethereum/EIPs · GitHub: EIPs#12301 fix(txpool): separate verification floor from node headroom by SIDDHANTCOOKIE · Pull Request #14992 · NethermindEth/nethermind · GitHub: nethermind#14992 Update EIP-8250: let a transaction scope its nonce keys to the payer by AnkushinDaniil · Pull Request #12422 · ethereum/EIPs · GitHub: EIPs#12422

Mission 2028 puts formal verification at its core! EthLib is a central part of this effort, and we've already made tremendous progress. We need more eyes, more contributors, and more agents to help push this massive effort forward! ethereum/EthLib

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