We introduce an assertion-based logic specifically designed for local reasoning about probabilistic programs featuring unbounded loops. Distribution formulas and their extensions facilitate the representation of invariants for unbounded loops in probabilistic programs. The assertions connected by separating conjunction exhibit probabilistic independence, which more intuitively displays the mutually independent properties of variables and ensures that the logic supports local reasoning. We prove the soundness of our logic and showcase its effectiveness through the formal verification of a wide range of examples including probabilistic inference in Bayesian networks and security analysis of cryptographic schemes.