Exploring Automatic Model-Checking of the Ethereum specification (tech. report)
We have published the report on model checking of accountability in the 3-slot finality protocol for Ethereum Foundation...
In Q3-Q4 of 2025, Thomas Pani, Jure Kukovec, Thanh Hai Tran, Roberto Saltini, and I worked on model checking of the brand-new (back then, under development) 3-Slot Finality protocol for Ethereum Foundation. Due to a large scope of the protocol, we limited ourselves to the accountability of the protocol.
Model checking of accountability for 3SF happened to be quite challenging and, thus, exciting! We have thrown a lot of tools at the protocol, including Apalache, Alloy, CVC5, and Kissat. We could not break accountability with all these tools. It is worth noting that this verification problem poses a serious challenge for all these tools. See the details and our thoughts on this in the report.
I am going to write my thoughts on how the model checkers could be improved to address protocols like 3SF in a longer blog post.