<p>Lane-changing algorithms play a critical role to ensure passenger safety and traffic efficiency in the dynamic and stochastic environment of Autonomous Vehicles (AVs). Despite the safety-critical nature of lane-changing algorithms, they are generally analyzed using computer simulation, which, due to its sampling-based nature, cannot guarantee capturing all the corner cases. As a more rigorous alternative, we advocate using probabilistic model checking for the formal analysis of lane-changing algorithms. The proposed approach utilizes Markov Decision Processes (MDPs) to model the stochastic dynamics of AV lane-changing maneuvers and allows us to formally verify properties specified in Probabilistic Computation Tree Logic (PCTL). For illustration, we formalized the MOBIL (Minimizing Overall Braking Induced by Lane Changes) algorithm with the Intelligent Driver Model (IDM), i.e., a widely used framework for AV lane changing, and formally verified its critical properties, such as safety and lane-change efficiency, temporal performance, and system robustness under dynamic traffic conditions using the probabilistic model checker PRISM.</p>