A Lean proof sharpens Ethereum’s fast-confirmation work

Ethereum researcher Francesco D’Amato reports that the Fast Confirmation Rule now has a safety proof in Lean, a proof assistant that checks formal mathematical arguments. His account describes agents doing much of the verification work over several days, with a model closely following the consensus specification.

Fast confirmation is distinct from finality. D’Amato describes confirmation in about 24 seconds under additional assumptions, rather than waiting roughly 13 minutes for finality. The proof concerns safety under those assumptions; it does not remove the need to understand them.

Adapting the model to the upcoming Gloas changes exposed a subtle fork-choice bug, according to the researcher. He says the specification was corrected and the updated verification then succeeded. This is a concrete example of checking how an existing property survives a surrounding protocol change.

ETH Canal perspective: faster research tools are useful when their output can be checked. For teams relying on confirmation timing, the valuable follow-up is to understand the rule’s assumptions and the exact behavior their product needs. A short confirmation estimate should not quietly become a promise of final settlement.