Formally verified proof of decoupled consensus moves faster finality closer

Researcher Francesco D'Amato (fradamt) shared a formally verified, machine-checked proof of Ethereum's decoupled consensus protocol — the favored model for 4–8× faster finality — calling it "one step closer" to that target.

The fradamt/verified-consensus repository models decoupled consensus as an executable state machine in Lean 4 and proves its consensus guarantees covering the confirmed, stable, and finalized chains, with no sorry and no project-specific axioms. The results assume honest committee majorities and bounded delivery after GST, among other premises listed in the proof's premise ledger. The Ethereum account amplified the announcement on X.