在计算机科学和软件工程领域,软件工程师采用软件测试的方法来验证计算机软硬件系统的正确性,这样的测试虽属于常规方式,但有时耗费巨大。工程师还会采用形式化验证技术来进行相关的正确性验证工作。形式化验证就是根据某些数学化的形式规范,利用严格的数学化方法来验证软硬件系统的正确性。它基于数理逻辑,适用于大部分的软件、硬件系统,如:航天、医疗、人工智能和区块链系统等。本论文来源于中科院软件研究所,并聘请了国外知名大学专家进行项目主导,以此开发出具有自主知识产权形式化验证工具。国内目前缺少自主研发的供其使用的验证工具,在国外所开发的交互式验证系统工具的使用中,需要用户来进行大量且繁琐的文本编码操作,这使得团队培训和验证操作的费用以及时间代价非常高昂。作者在参与项目的开发工作中,首先是明确项目需求,进行可行性分析以及明确总体目标,其次在概要设计中,作者依据平台需求分析设计了系统的整体架构和各模块的划分,并画出相关的流程图和架构图。在概要设计的基础上,作者基于Vue.js框架、HOL系统设计原理、Ajax异步交互技术、Lark解析工具等来对系统各模块进行设计与开发。在系统功能主界面开发过程中,作者积极搜集并学习了相关领域最新技术资料。作者学习并掌握了Ajax异步交互技术的原理和实现,在此基础上设计实现了基于Flask的系统逻辑层,这使得系统运行更加快捷。在数据定义模块中,作者依据HOL系统原理以及霍尔逻辑原理,来设计实现了计算机程序验证数据类型。在数据处理模块中,笔者使用了Lark解析工具,这使得证明数据解析和匹配的过程准确、清晰。在本验证系统中共包括了验证界面实现、证明数据交互、证明数据定义、证明数据处理、证明数据管理等五个模块。作者主要参与完成了验证界面实现、证明数据定义、证明数据交互以及证明数据处理等四个模块。目前验证系统已能够完成简单的程序验证和定理证明工作,后期还会有其他的更加完备的功能添加进来。