All roads lead to Cambridge

A summary of the 4 workshops organized by the Ethereum Foundation

Last year, we participated in the Ethereum Foundation's Post-Quantum Cryptography in Cambridge. The main topics were the LeanVM, designed for Ethereum's new post-quantum secure signature scheme based on XMSS, the new roadmap for Ethereum and hash functions. Formal verification was also a topic, helping secure both the signature scheme and the virtual machine. The event gathered researchers from several teams. Migrating to the new lean signatures provided not only quantum resistance but also an increased performance and reduced the staking requirements for validators. AI was already present, but was sparsely used. We then left Cambridge to return home and participate in DevConnect in Buenos Aires.

Late November, Claude 4.5 was released and things started accelerating: creating new features and testing alternatives starting getting cheap. With a host of new models, attacks on several cryptographic primitives started to appear and research on several areas accelerated.

This year, Google released a paper showing that the estimates for running Shor's algorithm to break elliptic curve cryptography were wrong. The use of autoreseach allowed to improve the running times for several algorithms. Even if quantum computers were not going to make it, it is possible that AI will find ways to take advantage of the algebraic structure of elliptic curves to find new and more efficient attacks. Therefore, it is necessary to improve the security of our systems by analyzing them more thoroughly, creating formal specifications, trying to attack them and replacing them by post-quantum secure alternatives.

The Ethereum Foundation organized a new series of workshops from the 10th to the 15th of October in Cambridge, following the success of the previous edition. This time, more than 120 researchers and engineers attended, working on 4 different areas:

1. Post-quantum cryptography (10-12)
2. Formal verification (13-15)
3. Fast finality (13-15)
4. Hash functions and cryptanalysis (13-15)

Formal verification was one of the hottest topics, having its own dedicated workshop and featuring extensibly in the others, providing the much needed security guarantees for implementations and optimizations using autoresearch.

The post-quantum workshop touched several aspects that are crucial for Ethereum's future:

• zero-knowledge virtual machines
• more efficient Merkle tree structures
• efficient stateless signatures for transactions that can be run in hardware wallets
• stateful signatures for Ethereum consensus
• formal verification for signatures, virtual machines, and recursion
• the decision tree for selecting the hash function

The current choice for stateless signatures is SPHINCS+, which is a hash-based signature. While signature sizes are larger and signing times high, recent improvements have shown that it is possible to sign in around 1.5 seconds using a Ledger hardware wallet with the variant SPHINC+G (adding grinding and precomputation).

As for stateful lean signatures, the current autoresearch challenge has found better parameters, leading to 50% smaller signatures or smaller number of cycles needed to verify such signature (which is crucial for aggregation).

Formally verifying recursion (a key component both for execution and signature aggregation) was one of the big open problems that were discussed. Current proof systems are proven secure using the random oracle model, but the assumption for recursion is based on the plain model. There are some theoretical questions on which is the best way to prove security and the use of heuristics. The Fiat-Shamir transformation was discussed in several talks, since it is one of the crucial components of proof systems. Having a clear and formally verified spec for recursion is essential to optimizing its performance using AI agents. There were also several discussions regarding compilers and new tooling to make formal verification easier.

Regarding the hash function, BLAKE2s seems to have an edge, since it is very efficient to prove using binary fields (for example, Flock), and has been around for several years without an attack. SHA-3 or variants are more expensive to prove, while BLAKE3 is less battle tested than BLAKE2. There is an ongoing challenge using AI to try to break or attack some of the existing hash functions.

The event was also a great opportunity to meet with several friends and discuss new ideas, developments and get more information on different initiatives. There were 3 dinners organized by the EF, including one with 120 people!

The future looks quite challenging with all the advances and threats from both the AI and quantum computers. However, Ethereum has a very clear roadmap and strategies to face these challenges and can bring together more than 120 people to discuss and work on post-quantum secure cryptography, hashes, formal verification, fast-finality, consensus and deliver good engineering.