形式化验证是目前已知的确认程序正确的最可靠的方法，是安全攸关领域开发高可信软件，保证软件系统的正确性、安全性和可靠性的必备工具。本公司推出了用于C程序验证的形式化验证工具--科创验证器，和为方便用户学习形式化验证方法与技术的云学习平台--科创验证器学习版。
       科创验证工具采用的是基于演绎推理的形式化验证技术，结合Hoare逻辑演算，形状图逻辑推理，自动定理证明等技术，根据程序员给出的有关程序功能的形式化描述（规约），结合程序代码进行演绎推理，保障通过验证的程序符合形式化规约的约束，也就是说程序是正确的。