Abstract This paper presents a modular approach to verifying the vector module of PETSc, a widely used library in scientific computing, using the CIVL model checker. Our approach relies on the creation of stub functions, which serve a dual purpose of specifying the intended behavior of individual PETSc functions and providing an abstraction for called functions to allow efficient verification of callers. This facilitates the use of symbolic execution and model checking to establish the correctness of isolated functions. Our work contributes to the ongoing effort to enhance the reliability of high-performance computing libraries and proposes an effective verification strategy for complex scientific software.