AI is making Ethereum more ambitious. You might have heard about the challenges that blockchains face in a post-AI world, and while security assumptions will surely be stress-tested in the coming months and years, there is another side to it. I believe AI will let us speedrun towards a world that's both more secure and feature-rich. As we look towards Ethereum's first post-AI upgrade, Hegotá, the R&D community is asking itself what increasingly powerful tools could help us do differently: > How far can we push both security and iteration speed? > How much of the design space can we examine before committing to one? > How easily can we test the interactions between complex features? My recent formal verification work @ethlabs_org has given me some reasons to be optimistic about these, as work that would have previously not even been attempted is now being done by agents in days. In September, I posted about using formal verification as part of designing a new consensus protocol. This time, I want to tell you about formally verifying something already fully specified and in production: Ethereum's Fast Confirmation Rule (FCR). If you are not familiar with FCR, it lets applications confirm Ethereum blocks in seconds, roughly 30x faster than waiting for finality, under additional assumptions (from waiting 13 minutes to 24 seconds!). It also further solidifies Ethereum L1's case as an asset hub and center of gravity for the onchain economy. FCR now has a safety proof in Lean, closely modeling the rule in the consensus specs, which is the source of truth for Ethereum's consensus clients. Some takeaways: > FCR is safe! Under its assumptions, confirmed blocks remain canonical. On top of the manual proofs from the paper, we now have Lean proofs of this for the actual spec, additional evidence for applications considering FCR! > The bulk of the formal verification work took just a 4-5 days (check out the animation!), with agents working mostly unsupervised. We should be very ambitious about using this as a tool at scale. > After verifying the current rule, it was easy to adapt the model to the upcoming Gloas changes. Immediately, this surfaced a subtle bug caused by changes to fork choice. The problem was in the spec itself and not a gap in the model. The safety proof would not go through, and the agents could precisely pinpoint what was causing it to fail. The bug is now fixed, and formal verification of the corrected protocol goes through. Iteration is never quite over, even for "finished" features like FCR, because the protocol keeps evolving around them. A formal model lets us ensure that key properties keep holding throughout the evolution of the protocol. With these capabilities, Ethereum can and should keep upgrading faster, tightening fork timelines and exploring more ambitious features, while still raising the security bar. This picture has been getting much clearer over the past few months, and the past week confirmed it for me, as @drakefjustin and @corcoranwill brought together 100+ Ethereum researchers, cryptographers and formal verification experts in Cambridge for six days of workshops on post-quantum cryptography, formal verification and fast finality. Beyond its own workshop, formal verification was the omnipresent star of the week: everyone is using Lean and doing amazing things with it! Piece by piece, Ethereum's technological core is being rebuilt for the post-AI age. The excitement was palpable, the sense of optimism was pervasive, and every talk and conversation carried a level of ambition I'd never seen before. The Ethereum R&D machine is upgrading itself, and we will see the outcome of that on the network sooner than you think.