<p>In Consensus layer of Ethereum, the Beacon Chain is the main component that maintains details related to validator status, attestations, penalties, and rewards according to the behavior of validators. A large amount of Ethers (ETH, Ethereum cryptocurrency) of different validators are at stake in Consensus layer of Ethereum right now and any change in ETH value due to slashing or rewards is managed by the Beacon Chain. Beacon Chain is a safety-critical system and any error or bug in it can affect the complete network of Consensus layer of Ethereum. A single mistake can cause a huge loss of ETH on stake and problems such as invalid block insertion and security attacks. The reference implementation of Beacon Chain developed by the Ethereum Foundation gives a complete operational description of the Beacon Chain. In this work, we focus on the formal modeling and verification of reference implementation of the epoch processing of Beacon Chain to ensure that the Beacon Chain epoch mechanism is designed correctly and robustly and that there exists very little chance of any bug. To achieve this goal, we utilize model checking, the most effective technique based on formal methods that is used to ensure the correctness of safety-critical systems. In this work, formal modeling is done for the epoch processing operations of the Beacon Chain using Process Meta Language (PROMELA). For verification purposes, safety properties are defined for each epoch processing operation of the Beacon Chain, and we formalize these properties using Linear Temporal Logic (LTL). Formal models and LTL formulas are given as input to the model checker to check whether these formal models satisfy LTL formulas. The SPIN model checker is utilized for the formal verification of the Beacon Chain.</p>