望安科技与军科院签订合作协议，为代码的高安全性、可靠性保驾护航！

军科院和望安科技在经过多次深度交流、探讨后，双方已经达成合作意向，并顺利签订合作协议。

军科院是军事科学研究中心，是计划协调军事科研工作的机构。

军事软件的应用已经渗透到军事领域的各个角度，由于应用环境的特殊性，决定了军事软件的信息关系更为复杂，军科院对软件代码质量的安全性、可靠性、软件开发的高效性提出了更高的要求。

望安科技是以“形式化验证”为核心技术的安全服务及产品提供商，致力于为国家重大项目、核心软件及企业提供安全认证保障。安全产品及服务已应用于航空、航天、国防、区块链、互联网金融、芯片设计制造、轨道交通等重大领域。

形式化方法是一种基于数学的使用精准化规范说明来开发和验证计算机软硬件的一种技术，将形式化方法用于软件和硬件设计，可以提高设计的可靠性和安全性。鉴于军工软件的在安全可靠性的高度需求，形式化方法依托其特性在领域内表现出巨大的优势。形式化代码生成工具软件对推动军用软件能力和质量效率的不断提升发挥了积极作用。

1.通过提供的形式化代码生成工具软件，提高软件的开发效率

模型驱动代码的自动生成，能够有助于提高嵌入式实时系统的软件开发的自动化水平，缩短软件开发周期，减少人工写代码的工作量和编码过程中出错的可能性。

2.通过形式化C代码自动化验证器，提高代码的的质量

工具提供了用于描述功能的形式规约语言，基于形式规约语言注释的源代码形式化自动验证器，以及良好的验证状态、验证结果与源代码功能错误定位的界面展示。包括通过数学逻辑对C文件的代码逻辑进行验证，保证代码的正确可靠性。

目前，软件已经广泛应用到军事领域的各个系统，而国家军事领域信息安全关乎着国家安全，其软件系统的安全性、可靠性至关重要。同时随着国家军事力量的不断发展，军事科学技术对高速研发工具的需求极为迫切。

望安科技基于核心技术”形式化验证“，在军事领域保障军事软件系统的安全性、可靠性及研发自动化，发挥着重大作用。望安科技将持续研发，助力军事领域信息安全，提高军事领域软件自动化水平。