Fortifying Integrity, Traceability, and Operational Efficacy in Blockchain-Based Examination Management Through Formal Verification with TLA+

The current research sheds light on the potential of blockchain technology in contributing towards enhancement of security, transparency, and efficiency in an educational system. By securely storing academic records on Ethereum’s decentralized ledger, the system automates administrative tasks, reduces fraud, thereby improving reliability and accessibility for students and institutions. The proposed smart contract facilitates a user-centric examination management system, addressing enduring challenges in education by providing an auditable trail of academic transactions. The research employs TLA+ (Temporal Logic of Actions) to model and verify the behaviour of smart contracts in a blockchainbased educational examination management system. The study unfolds in several phases: it begins by using TLA+ as a formal specification language to eliminate ambiguities inherent in natural language descriptions. Subsequently, the system is modelled with distinct states and actions that describe state transitions. Temporal logic is introduced to specify properties over time, ensuring the system operates correctly under concurrent conditions. The model checker TLC evaluates the state-based model for correctness, safety, and liveness. The mapping of TLA+ constructs to Solidity code demonstrates how formal specifications translate into executable smart contracts. Hoare Logic is applied for verifying the correctness of key functions by establishing pre-conditions and postconditions for ensuring desired outcomes.