Formal modeling and verification of GRANDPA finalization safety in polkadot

Abstract Polkadot enhances its security and reliability through the GRANDPA(GHOST-based Recursive Ancestor Deriving Prefix Agreement) finalization protocol, which provides deterministic and irreversible block finalization via structured validator voting rounds. Finality is a fundamental component of...

Celý popis

Podrobná bibliografie

Hlavní autoři:	Muhammad Rashid, Nazir Ahmad Zafar, Lal khan, Mohammad Zubair Khan, Abdulrahman Alahmadi
Médium:	Artigo
Jazyk:	Inglês
Vydáno:	Nature Portfolio 2026-05-01
Edice:	Scientific Reports
Témata:	Blockchain Polkadot GRANDPA Model checking SPIN
On-line přístup:	https://doi.org/10.1038/s41598-026-51047-3
Tagy:	Přidat tag Žádné tagy, Buďte první, kdo vytvoří štítek k tomuto záznamu!