Scientific computing (SC) involves using advanced computing capabilities to understand and solve complex physical problems. With the increasing complexity of physical models and a rise in demand for high-performance computing (HPC) resources, errors can occur at all levels of abstraction in the computing process, significantly impacting the process of computer driven-scientific discovery and decision-making. Thus, correctness in scientific computing remains a formidable challenge. Prior works have attempted to verify a numerical program end-to-end but fall short in terms of scalability in the proof process, and target an idealized implementation of a numerical program. This project addresses this gap by developing a scalable verification framework, which directly targets application SC libraries written in Low Level Virtual Machine (LLVM)-compatible programming languages, like C/C++, Fortran and Julia, instead of an idealized implementation. The project's novelties are mechanized functional models for SC algorithms, accuracy and stability proofs of critical numerical algorithms in reduced- and mixed-precision floating-point (FP) formats, and the development of evidence and assurance cases for guaranteed correctness of future ports to new accelerated hardware. The project's impacts are an increased productivity of model developers, by providing a framework for root cause analysis of numerical bugs, and strong assurance cases for highly performant SC applications. This pr