Researchers from the Ethereum Foundation have developed and formally verified a protocol model that decouples finality from block production and fork choice. This modular approach aims to reduce finality time from the current 16 minutes to under a minute, eventually targeting just seconds. The model uses smaller committees of 256 to 512 validators for fast block production, while the full validator set maintains a separate finality gadget. The formal verification was conducted using the Lean 4 proof assistant, providing mathematical guarantees for properties such as safety and finalization. The “strawmap” roadmap outlined by Vitalik Buterin targets finality improvements by 2029.
Source: Read the original article

