Prior work has described an algebraic framework for proving the correctness of Prim's and Kruskal's minimum spanning tree algorithms. We prove partial correctness of an additional minimum spanning tree algorithm, Boruvka's, using the same framework. Our results are formally veri ed using the automated deduction capabilities of the Isabelle proof assistant. This further demonstrates the suitability of the algebraic framework as a sound abstraction for reasoning about weighted-graph algorithms.