Formal modeling and verification of GRANDPA finalization safety in polkadot
Muhammad Rashid, Nazir Ahmad Zafar, Lal khan, Mohammad Zubair Khan, Abdulrahman Alahmadi · 2026
Read Formal modeling and verification of GRANDPA finalization safety in polkadot by Muhammad Rashid, Nazir Ahmad Zafar, Lal khan, Mohammad Zubair Khan, Abdulrahman Alahmadi (2026) in the Tower of Babel, a free online library of public-domain works preserved in clean, searchable text. No sign-up. The full text is served as a plain-text file at a predictable URL, where text is present: https://antarctic-labs.com/tower-of-babel/pmc-13338187.txt.
Description
Muhammad Rashid and his co-authors wrote this work in two thousand twenty-six. It checks GRANDPA, the Polkadot tool that makes blocks final through rounds of votes by validators. Once final, a block can not be undone. If this step fails, trust in the whole chain can break.
The team first set the tool out as clear steps, for authority updates, the pre-vote, the pre-commit, the vote count, and the final step. They then built a Promela model of how voters act. Two safety traits, set in Linear Temporal Logic, were checked with SPIN: no clashing final blocks, and final blocks stay final. They tracked states seen, moves, time, memory, and search depth, and found some traits drove the growth of the search far more. This shows such checks work, and lays ground for work on liveness, worse attacks, and harder Polkadot set-ups.
Catalog record
| CREATOR | Muhammad Rashid, Nazir Ahmad Zafar, Lal khan, Mohammad Zubair Khan, Abdulrahman Alahmadi |
|---|---|
| YEAR | 2026 |
| COLLECTION | PAPERS |
| FORMAT | TXT |
| FILE SIZE | 107 KB |
| VERSION | 1.0 |
| LICENSE | CC BY 4.0 |
| RIGHTS | CC BY |
| SOURCE | Europe PMC |