关键词: 超长整数运算, 原型验证系统（PVS）, 一致性验证, 形式规范, 定理证明

Abstract: The operation of super long integers is the basic component of the application of modern cryptosystem, and its correctness relates to the application value of the system. In order to verify the consistence between the requirement analysis and the design goal of these algorithms, the correctness of the algorithms are formally verified using PVS. This paper introduces the addition and subtraction algorithms for super long integers and analyses the design idea of these algorithms, presents the formal specification of super long integers and the algorithms. Then by describing the property of the algorithms as theorems, the consistency checking is converted to a problem of theorem proving. These property theorems are proved with the theorem prover of PVS, so the design requirements of these algorithms are satisfied.

Key words: operation of super long integers, Prototype Verification System（PVS）, consistency verification, formal specification, theorem proving