Formal modeling and verification of GRANDPA finalization safety in polkadot

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 consensus, as any failure in this process can compromise the integrity and operational continuity of the entire blockchain. Ensuring the safety and correctness of GRANDPA finalization is therefore crucial to prevent critical failures and maintain network trust. This work presents a formal verification study of the GRANDPA finalization mechanism using model checking techniques. The protocol is first analyzed in detail and represented as structured algorithms encompassing authority updates, Pre-Vote, Pre-Commit, vote aggregation, and finalization phases. A comprehensive Promela model is developed to capture the complete behavior of validators and the interactions across voting phases. Key safety properties, including no conflicting finalization and finality irreversibility, are formalized using Linear Temporal Logic (LTL) and systematically verified using the SPIN model checker. During verification, multiple performance and scalability metrics are analyzed, including total states visited, transitions explored, verification time, memory usage, search depth, and property-specific verification complexity. The analysis identifies properties that significantly influence state-space growth, providing insight into the structural complexity and computational demands of the protocol. This study demonstrates the effectiveness of formal model checking for evaluating blockchain consensus protocols and establishes a foundation for future verification efforts, including liveness properties, extended adversarial scenarios, and verification of more complex consensus configurations within the Polkadot ecosystem.