Laplacian matrices are essential algebraic representations of network systems, which facilitate the description of topological characteristics, such as connectivity and symmetry. However, a critical issue emerges when the Laplacian matrix of a network is inherently singular, i.e., its inverse does not exist. In this case, it is crucial to use the generalized inverse of the matrix, known as pseudoinverse. In this paper, we provide a rigorous formalization of the pseudoinverse of the Laplacian matrix representing a weighted graph within higher-order logic theorem proving. Particularly, we formalize in Isabelle/HOL the generic concept of a matrix pseudoinverse that is applicable for both singular and nonsingular matrices. We then formalize the pseudoinverse of a Laplacian matrix and verify its classical properties. As an application, we formally verify the Kirchhoff index of a two-horizontal bridge circuit network.