We formalize the proof of Reingold's Theorem that SL=L (STOC'05) in the theory of bounded arithmetic VL, which corresponds to ``logspace reasoning''. As a consequence, we get that VL=VSL, where VSL is the theory of bounded arithmetic for ``symmetric-logspace reasoning''. This resolves in the affirmative an old open question from Kolokolova's PhD thesis (2005) (see also Cook and Nguyen (2010)).

Our proof relies on the Rozenman-Vadhan alternative proof of Reingold's Theorem (RANDOM'05). To formalize this proof in VL, we need to avoid reasoning about eigenvalues and eigenvectors (common in both original proofs of SL=L). We achieve this by using some results from Buss-Kabanets-Kolokolova-Kouck\'y (APAL, 2020) that allow VL to reason about graph expansion in combinatorial terms.