ethlambda at the Cambridge workshops: post-quantum signatures, fast finality, and formal verification

From October 10 to 15, the Ethereum Foundation brought more than 120 researchers and engineers to Cambridge for four workshops: one on post-quantum cryptography, followed by three parallel tracks on formal verification, fast finality, and hash functions and cryptanalysis. The event built on last year's post-quantum workshop in the same city, and the sense of urgency has grown since then. A recent Google paper revised the resource estimates for breaking elliptic curve cryptography with Shor's algorithm, and AI-assisted research has made both building and attacking cryptographic systems far cheaper. Transitioning to post-quantum primitives and proving the correctness of both the primitives and their implementations are now near-term tasks.

We were invited to share our experience with post-quantum signatures in leanConsensus. Topics ranged from leanVM performance and smaller post-quantum signatures and proofs to checking that Lean 4 specs match deployed binaries and settling on a faster finality algorithm.

Running devnets with post-quantum signatures

We've spent months running leanConsensus devnets with post-quantum signatures, and we brought that experience to the workshop. We explained how we scaled from 32 to 4,096 validators, discussed the architectural changes we tried along the way, and outlined directions worth exploring next. We also gave a joint presentation with the Lantern client team on the post-quantum transition from the perspective of leanConsensus client developers.

Signatures and hash functions

On the execution layer, transactions need stateless signatures, and the current candidate is SPHINCS+, a hash-based scheme. Its signatures are larger and take longer to generate than those used today, but a variant using grinding and precomputation can now generate a signature in about 1.5 seconds on a Ledger hardware wallet. An autoresearch challenge focused on its parameters has also identified improvements that can cut signature size by 50% or reduce the number of cycles needed to verify a signature, which matters for aggregation.

As for the hash function, BLAKE2s appears to have the edge. It is efficient to prove over binary fields (Flock is one example) and has gone years without a practical attack. SHA-3 and its variants are more expensive to prove, while BLAKE3 has received less scrutiny than BLAKE2. An AI-driven challenge to attack the candidate hash functions is also underway.

Building a decoupled consensus prototype

During the week, we also started working on a decoupled consensus prototype in ethlambda. Discussions on fast finality converged on an algorithm inspired by Goldfish, which we covered in a previous post. We'll leave the details to the official proposal, which is expected in the weeks leading up to Devcon.

An early version of the idea is discussed in Unblocking faster finality with decoupled consensus, though the algorithm that emerged from the workshop is arguably simpler.

Formal verification

Formal verification had its own workshop and came up constantly in the other three. The reason is practical: a precise, verified spec makes it safe to hand optimization work to AI agents, since their changes can be checked against it.

The formal verification talks kept returning to one question: how do you make sure a Lean 4 spec matches what the deployed binary actually does? Several approaches were presented, and we might see some of them applied in the coming weeks. Other talks made the case for migrating the protocol specs to Lean 4 and explored how to get there. They also covered problems people have encountered while working with Lean 4, as well as new compilers and tooling to make verification easier.

Recursion was one of the big open problems. It underpins both execution proofs and signature aggregation. However, current proof systems are proven secure in the random oracle model, while recursion relies on assumptions in the plain model. How best to bridge that gap and how much to rely on heuristics remain open questions. The Fiat-Shamir transformation came up in several talks for the same reason.

We're also putting formal verification into practice in ethlambda. We've started implementing parts of the client in Lean 4 so we can prove their correctness. Expect more on this soon.

What's next for us

We're doubling down on beacon chain support and have started work on experimental features for the upcoming forks.

It was a packed week of talks, workshops, and conversations, and we're already looking forward to next year's edition. Thanks to the organizers for putting the workshops together and to everyone who presented.