The VQCS is a formal verification project in Coq, which stands for "Verified Quantity Calculus System". We have modeled physical quantities, units, and dimensions, supporting calculations with units, and provide support for the International System of Units (SI), thereby enabling the verification of issues related to units.
Below are main links of this project: