The rapidly evolving landscape of scientific computing, led by approximate computing approaches and heterogeneous hardware, is leading to the reimplementation of classical numerical algorithms. For the safe deployment of these new variants, they need to be verified correct with respect to their classical counterparts. These classical algorithms are extensively studied by mathematicians, but generally are not mechanized in proof assistants.

In this work, we present our preliminary work on developing a general framework for mechanizing different variants of a classical numerical algorithm. We start with a fundamental orthogonalization algorithm, the Gram-Schmidt process, and demonstrate a proof structure for verifying the correctness of a numerically stable variant (Modified Gram-Schmidt) by way of exact Real equivalence with the corresponding classical algorithm (Classical Gram-Schmidt).