NethermindEth

[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

LeanCIL: formal proofs for your compiled C#, checked by Lean Microsoft's October Patch Tuesday fixed over 1,400 CVEs, more than in all of 2025, and much of that came from AI-driven bug finding. Attackers have the same tools, and more of our code is now written by models that produce convincing code with subtle bugs. “The tests pass” isn’t a strong enough guarantee any more for code that matters. A couple of months ago I proposed an official Lean semantics for C# on csharplang (#10314). One reply asked why not do it at IL level, so it covers F# and everything else that compiles to IL. That’s what I built. You point it at a Release build and a method: leancil extract bin/Release/net10.0/MyLib.dll "Arithmetic::Add(ulong,ulong)" artifacts/Add leancil verify artifacts/Add --proof proofs/Add.lean and it proves your theorem against the IL Roslyn actually emitted. Change the implementation and the same proof fails. Supported (.NET 10, x64 and ARM64, 64-bit little-endian): - Integer arithmetic, including checked, with overflow and divide-by-zero as exact faults - Structs with explicit and sequential layout, enums, ValueTuple - Span<T>, ReadOnlySpan<T>, slicing, MemoryMarshal.Cast/AsBytes, BinaryPrimitives - Arrays, stackalloc, unsafe pointers with checked provenance - Generic methods and structs (proved per concrete type argument), constrained interface calls on structs - Function pointers and tail calls - Collection-expression lookup tables (static ReadOnlySpan<T> Table => [...]) - Selected Vector128/256/512, SSE, AVX2, AVX-512 and AdvSimd intrinsics; IsSupported branches are resolved for the chosen hardware profile - throw new ArgumentException(...) and similar, proved as the exact exception Not supported: float/double, class instances, try/catch/finally, ordinary recursion, virtual dispatch on classes. Unsupported code is rejected with a diagnostic, never silently accepted. The best fit right now is allocation-free integer code where a bug is a security bug: parsers, hashing, big-integer arithmetic, SIMD kernels. NethermindEth/LeanCIL

LeanCIL: formal proofs for your compiled C# and F#, checked by Lean Microsoft's October Patch Tuesday fixed over 1,400 CVEs, more than in all of 2025, and much of that came from AI-driven bug finding. Attackers have the same tools, and more of our code is now written by models that produce convincing code with subtle bugs. “The tests pass” isn’t a strong enough guarantee any more for code that matters. A couple of months ago I proposed an official Lean semantics for C# on csharplang (#10314). One reply asked why not do it at IL level, so it covers F# and everything else that compiles to IL. That’s what I built. You point it at a Release build and a method: leancil extract bin/Release/net10.0/MyLib.dll "Arithmetic::Add(ulong,ulong)" artifacts/Add leancil verify artifacts/Add --proof proofs/Add.lean and it proves your theorem against the IL Roslyn actually emitted. Change the implementation and the same proof fails. Supported (.NET 10, x64 and ARM64, 64-bit little-endian): - Integer arithmetic, including checked, with overflow and divide-by-zero as exact faults - Structs with explicit and sequential layout, enums, ValueTuple - Span<T>, ReadOnlySpan<T>, slicing, MemoryMarshal.Cast/AsBytes, BinaryPrimitives - Arrays, stackalloc, unsafe pointers with checked provenance - Generic methods and structs (proved per concrete type argument), constrained interface calls on structs - Function pointers and tail calls - Collection-expression lookup tables (static ReadOnlySpan<T> Table => [...]) - Selected Vector128/256/512, SSE, AVX2, AVX-512 and AdvSimd intrinsics; IsSupported branches are resolved for the chosen hardware profile - throw new ArgumentException(...) and similar, proved as the exact exception Not supported: float/double, class instances, try/catch/finally, ordinary recursion, virtual dispatch on classes. Unsupported code is rejected with a diagnostic, never silently accepted. The best fit right now is allocation-free integer code where a bug is a security bug: parsers, hashing, big-integer arithmetic, SIMD kernels. NethermindEth/LeanCIL

AI now finds bugs that survived decades of human review, and writes code that looks right but isn’t. Tests can’t keep up. LeanCIL: formal verification for .NET Proofs about compiled C# and F# (any dotnet lang), for every input, checked by @leanprover NethermindEth/LeanCIL

Show HN: LeanCIL – Prove properties of compiled .NET code in Lean 4

If you run Nethermind on Hoodi, upgrade to 2.2.1 before 26 Oct. On today’s All Core Devs call, client teams postponed the Glamsterdam fork on Hoodi to review a change to its specification. A new date will follow. Meanwhile, upgrade your Hoodi node now: github.com/NethermindEth/nethermind/releases/tag/… t.co

We successfully tested @Nethermind's standalone Rollup0 prover with the @etheconomiczone composer, including L1 proof acceptance and restart/recovery. One step closer to a public EEZ testnet with multiple prover clients! WIP draft: nethermind#13867

Dev log #25 Hardening p2p networking and shipping interactive CLI features in Rust Hi, glad you found your way here. I'm Yash, a developer who contributes to open source, mostly p2p networking and AI tooling. Each week I write up what I shipped, what broke, and what fixing it taught me. GitHub · X · LinkedIn · Portfolio --- TL;DR Sometimes the most satisfying weeks aren't about the volume of commits, but the weight of the problems you're solving. This week was a deep dive into the guts of p2p networking and CLI ergonomics, all in Rust. I managed to get 5 PRs merged across two key projects, totaling 2,203 additions. The highlight was definitely landing the new interactive mode in Trak and tightening up some potentially leaky connection logic in minip2p. What I Built Most of my energy this week was split between two very different but equally interesting Rust projects: minip2p and Trak. Hardening the p2p Layer: minip2p Working on minip2p always feels like a battle against the inherent chaos of the internet. When you're dealing with NAT traversal and relay servers, you can't assume anything works the way it says it does. I spent a good chunk of time in the NAT and relay-server logic. One of the more critical fixes was addressing how we handle NAT renewals. I realized we were being a bit too trusting of the relay's expiration timestamps. If you trust an external server to tell you exactly when your mapping expires, you're asking for a dropped connection. I pushed a fix to schedule renewals at half the lifetime, providing a much-needed safety margin. I also dug into the relay-server itself to ensure we’re properly counting finished HOP workers against the connection cap. In p2p, if you don't track your resource usage with surgical precision, you end up with "ghost" connections that eat up your capacity until the whole node crawls to a halt. On the swarm side, I tackled a gnarly edge case where abandoning a peer-closed stream wasn't properly acknowledging its dropped data. It’s one of those "invisible" bugs that doesn't crash the app but leads to weird state mismatches over time. Getting that fixed (and documented) makes the whole stream lifecycle feel much more robust. Better Exploration: Trak On the developer tooling front, I’ve been contributing to Trak. This week was all about making the tool more "explorable." The big win was landing the interactive mode. Previously, you had to know exactly what subcommand you wanted. Now, if you run trak with no arguments, it drops you into an interactive session. I also mirrored the --tree functionality from callers over to calls. When you're trying to map out a complex codebase, being able to see the call hierarchy as a tree is a game-changer. I ended up adding about 1,757 lines to Trak this week, which included a lot of work on the interactive match list ordering and driving a scripted interactive session against the binary to make sure the UI doesn't regress. Pull Requests It was a "clean sweep" week for PRs—5 opened, 5 merged. In minip2p, pull #323 and pull #322 were the heavy hitters for networking stability. The former dealt with that NAT renewal skepticism I mentioned, while the latter fixed the connection cap accounting in the relay server. I also landed pull #321, which ensures we're properly acking data when a stream is abandoned. These are the kinds of fixes that you don't "see" as a user, but you definitely feel when the network stays stable for days instead of hours. Over at Trak, pull #3 was the massive one. It introduced the interactive mode and changed the default behavior of the CLI. It’s always a bit nerve-wracking to change the entry point of a tool, but the feedback on the whole-branch review was solid, and I think it makes the tool much more approachable for new users. I also squeezed in pull #2 to add the --tree flag to the calls command, keeping the API surface consistent across the different search modes. Issues & Discussions While most things went smoothly, I did open one issue in minip2p that's going to need some brainpower next week. Issue #324 is about our manual-ack backpressure tests. Right now, the tests are a bit flaky because they interpret "the link has been quiet for 500ms" as "the link has stopped." In a real-world network (or even a busy CI runner), 500ms of silence doesn't necessarily mean the backpressure is working; it might just mean the CPU was busy elsewhere. I need to find a more deterministic way to validate that the data flow has actually paused without relying on wall-clock timers. Code Reviews I also spent some time in the dotnet-libp2p repo, helping out with some code reviews. Even though my own coding this week was 100% Rust, the p2p world is small, and the concepts carry over. I approved pull #303, which adds a fuzzing harness for core channels. Fuzzing is absolutely essential for networking code—if there's a weird state transition possible, a fuzzer will find it long before a human does. I also took a look at pull #299 regarding Yamux stream registration. Ensuring outbound frames don't get ahead of stream registration is a classic race condition in multiplexers, so it was good to see that getting tightened up. Tech Stack This was a pure Rust week. 8 commits, all in Rust. The line counts tell an interesting story: +2203 / -173. Usually, I like a higher deletion ratio (nothing feels better than deleting code), but this was a heavy feature-work week for Trak. Building out an interactive TUI (Text User Interface) and the associated logic naturally involves a lot of new code. I didn't hit a 7-day streak this week, but the work I did put in was high-intensity. Sometimes you need those gap days to let the p2p state machine logic settle in your head before you write the next line of code. What's Next Next week, I need to tackle that backpressure test flakiness in minip2p. Flaky tests are the bane of my existence, and I won't feel comfortable adding more features until the CI is rock solid. I'm also planning to keep refining the interactive mode in Trak—now that the foundation is there, I want to see if I can make the navigation even snappier. The p2p stack is feeling more stable, and the CLI tools are getting more powerful. It's a good place to be. See you in the next update!

Introducing Suno: DeFi yield backed by solar energy Hi r/RWA, I’m Nicolás, co-founder of Suno Finance. This is the founder’s view of our own protocol, so read it with that in mind. About Suno Suno (app.suno.finance) tokenizes cash flows from solar plants (curr. 25 solar farms, ~$5M AUM, some producing for six years). uWatt mints and redeems against USDC at min($1, NAV), with a 1.15x collateralization target (currently 1.12x). Deposit it in our ERC-4626 vault and you get c-uWatt, which compounds hourly at ~12% APY. It’s live on Ethereum with a LayerZero bridge to Polygon, and Base is coming soon. LP campaign There’s a c-uWatt/USDC Stableswap-NG pool on Curve mainnet (0x07830699FE73Eb90f1b3b466Ce88C38d4EEdd83B), with a gauge approved by Curve DAO. Staking LP tokens on StakeDAO earns boosted CRV at ~65% APR right now, settling near ~12% once TVL reaches $500k. You earn that on top of the solar yield and swap fees. Where the yield comes from New capital funds project finance loans to solar plants, underwritten on debt service coverage and repaid from energy revenue. A liquid sleeve of stablecoins and tokenized treasuries handles redemptions, with 10% of AUM reserved for them. The Colombian pipeline could absorb >$20M, and Ecuador and Brazil are next. Regulation and KYC Ensuro Re Ltd. issues uWatt in Bermuda under a BMA Class F license (DABA). It’s treated as a security and isn’t available to U.S. persons. You need KYC only to mint or redeem through the Suno Desk. Trading, LPing and staking are permissionless. Audit Nethermind reviewed the protocol in Sep 2026: github.com/NethermindEth/PublicAuditReports/blob/… Risks - Solar assets: yield depends on generation and offtakers paying. Collection is above 96%, though some older projects have had delays. The largest project is ~24% of the Reserve, and every asset is in Colombia, so local regulatory and FX risk apply. - Valuations: Suno pushes them on-chain using a public methodology. An Accountable proof-of-reserves dashboard is coming. - Liquidity: redemptions are instant while the liquid sleeve lasts. After that, exits depend on Curve liquidity or incoming cash flows. - Contracts: a 3-of-5 multisig holds the admin roles, and a timelock is on the roadmap. Curve, Stake DAO and LayerZero each add their own contract risk. About me I’ve spent 9+ years building and financing solar, and I co-founded Solenium in 2016 (a solar project construction company, >$40M annual revenue), Unergy (licensed utility company in Colombia) and Zentrack (hardware for solar farms). Questions and critical takes are welcome.

I built it instead 😁 Introducing LeanCIL - formal semantics for .NET CIL in Lean 4, with machine-checked proofs against actual compiled assemblies Not just C# - a foundation for verifying F# and other .NET languages too Let's formally verify dotnet NethermindEth/LeanCIL