The complexity of unit systems for physical quantities and their informal treatment pose potential risk of errors in engineering and mathematical reasoning. Moreover, existing formal verification tools lack support for reasoning involving physical quantities with units. To address this, we propose VQCS (Verified Quantity Calculus System), a formal system implemented in the Rocq theorem prover. Its main contributions are as follows. First, we construct a unit system based on dimensional analysis, defining the syntax and semantics of units while supporting both manual and automatic conversion between units of the same kind. Second, we establish a quantity calculus system over abstract data types. Third, we define concrete quantity calculus systems over the real numbers and real vectors, enabling unit-aware computations for common mathematical derivations in engineering applications. Finally, we instantiate the system with the International System of Units (SI) and provide several case studies demonstrating its practical utility. The VQCS framework is released as an open-source Rocq library, providing a verifiable infrastructure for quantity calculus in engineering modeling.