实验室以原创的自动推理研究成果为核心，研发了两类系统可信性自动验证工具：C 程序自动验证工具 Scavel C 和 PLC 程序自动验证工具 Scavel PLC。
该工具可验证程序多种缺陷类型：数组越界、被零除、指针无效、内存泄漏、有符号整数溢出、浮点数溢出、无符号整数溢出 、数值无效八种常见缺陷，还可验证其他与程序变量有关的自定义性质。具有直接验证源码、错误定位准确、验证结果准确、验证需求、设置灵活、验证过程快速高效、自动报告验证结果等特点。可广泛应用于航空航天、国防军工、核工业、卫星导航、轨道交通、网络安全、信息电子、电力、金融、通信等行业领域。
目前，该工具为涉及航空航天、国防军工、核工业、卫星导航、轨道交通、信息电子等领域的 20 余家单位提供了验证服务，显现了独有能力。
