关键词: 形式化验证, 定理证明, 斯托克斯定理, HOL Light

Abstract: Stokes’ theorem is one of the fundamental theorems in field theory, with extensive applications in fluid mechanics, electromagnetics, and other domains. However, in practical applications, the satisfaction of its prerequisite conditions is often not rigorously verified, which introduces certain risks. Therefore, it is necessary to validate Stokes’ theorem. This paper constructs a formal model of Stokes’ theorem based on its mathematical definition. By analyzing the mathematical proof process of the theorem, this paper derives the derivation methodology for its formal verification. Following the analysis, construction, and verification objectives, this paper ccompletes the formal proof of the theorem. Finally, the proven Stokes’ theorem is applied to the validation of the  pipeline flow design models.

Key words: formal verification, theorem proving, Stokes’theorem, HOL light