夜雨聆风
引言
一个你可能没听过的词，却关乎每一次发射。
2026年7月28日，央视《新闻联播》用近3分钟介绍了一位科学家——国防科技大学研究员王戟。
很多人第一次听到“高可信软件”这个词，就是从这条新闻里。
这个词听起来很学术，但它的含义非常直接：用数学方法，给大国重器的软件做“全身CT扫描”，从底层逻辑验证每一行代码是否正确。
它是国防装备的技术底座，也是当下“软件自主可控”国家战略中最硬核的方向之一。
01
什么是高可信软件？
一行代码，毁了一枚火箭。
上世纪90年代末，国外发生了一起震惊航天界的事故：某型运载火箭在升空几十秒后轰然爆炸。事后调查发现，事故的根源，竟然只是一行代码的错误。
当软件成为火箭、战机、舰船的“大脑”，怎样才能确保它在最关键的时刻绝不出错？
这个问题，指向的正是“高可信软件技术”。
通俗理解：
高可信软件是指可靠安全性和保密安全性标准极高的软件。
拆开来看：
· 可靠安全性：软件能正常运行，不会引发危险或灾难
· 保密安全性：软件能保护数据和信息不被窃取或破坏
普通软件的质量保障，靠的是测试——写一些测试用例跑一跑，看看有没有bug。但测试无法覆盖所有可能性。
而高可信软件用的是数学方法——从代码的底层逻辑出发，用严格的数学证明来验证代码的正确性。
打个比方：
· 普通软件测试 = 开车上路，看会不会出事（只能覆盖有限场景）
· 高可信软件验证 = 用数学公式证明这辆车在任何路况下都不会出事（穷尽所有可能性）
“高可信软件”通过给大国重器的软件系统进行‘全身CT扫描’、精准诊断，找出深层次隐藏的漏洞和隐患，是“软件的医生。
02
为什么这项技术怎么重要？
很多人知道高端芯片被外国垄断，但很少有人关注：开发、检测、验证软件的那些工具，同样被国外垄断。
我国航天、航空、轨道交通等关键领域，软件质量保障工具长期依赖进口。在航空航天领域，核心建模开发工具长期依赖国外商业软件，每年需花费数千万元引进。
一位科学家的“冷板凳”选择：
2003年，王戟与导师陈火旺院士等人发表了国内最早的“高可信软件工程技术”系统性论文。2004年，他开设了国内首个“高可信软件技术”研究生课程。
彼时，高可信软件在我国近乎“无人区”。有人劝他放弃——这个方向门槛高、难度大、周期长，短期内很难出成果。
王戟的回答很简单：“这个‘冷板凳’总要有人坐。”
三十多年来，他主持参与科研项目30余项，培养高可信软件技术骨干120多人，是我国高可信软件领域的主要开拓者。
03
高可信软件的产业化方向
高可信软件技术已从实验室走向产业，形成了多个落地方向。
方向一：代码质量检测工具
代表产品：泛联新安 CodeSense 代码静态分析平台
· 国内首款通过TÜV南德ISO 26262和IEC 61508功能安全认证的同类产品
· 覆盖C/C++、Java、Python等十余种编程语言
· 十万行级源代码3分钟内完成检测，准确率超过99%
· 已应用于航空航天、军工等关键领域
方向二：高可信建模开发工具
代表产品：上海控安 SmartRocket Modeler
· 对标国外航空航天领域高度依赖的SCADE Suite工具
· 已完成与银河麒麟V10操作系统的双向认证
· 支持SCADE Suite模型导入导出，方便用户从国外工具迁移
· 填补了国内高可信建模开发工具的空白
方向三：AI+高可信软件
代表产品：科大国创“基于形式化验证的AI智能体安全漏洞自动挖掘平台”
· 将高可信形式化技术与AI大模型结合
· 已在中国移动、航空航天等行业应用
· 其“国创星码编程AI助手”已在航空航天、运营商、金融、自动驾驶等领域试用
方向四：EDA芯片设计验证
形式化验证技术正在成为国产EDA（电子设计自动化）工具链的重要组成部分。
在芯片设计验证领域，形式化方法可用于验证复杂芯片设计是否符合预期规范，是突破EDA工具国产化难题的关键技术之一。国内多家EDA企业已将形式化验证作为重点攻关方向。
04
人物侧记：一个在轮椅上“冲锋”的人
我们再来说《新闻联播》用近三分钟讲述的这位科学家。
1983年，不满14岁的王戟考入国防科大计算机系。同年，我国首台亿次巨型机“银河-I”研制成功。“银河-I”软件系统的总负责人陈火旺院士，后来成为王戟的导师。
2013年1月，王戟突发主动脉夹层，经13小时手术保住了命，但双下肢高位截肢。
所有人都以为他会停下。但2015年，他摇着轮椅回到了实验室。
2021年，因肾衰竭他开始每周三次透析。三十多年来，他已历经700多次透析，却依然保持着“病房—实验室—教室”三点一线的工作节奏。
2025年，他被评为“全国自强模范”。
如今他仍在向人工智能可信问题发起攻关。他说：“科技强军的时间很紧，而我能够工作的时间远远不够。”
05
写在最后
你可能永远不会写一行代码，但每一次乘坐地铁、每一次航班起飞、每一次卫星升空——背后都有软件在运行。
而这些软件的可靠性，依赖的正是“高可信软件技术”这样的基础研究。
三十年前，这是一个“冷板凳”；三十年后，它正在变成国家战略的基石。
………
本文根据公开资料分析整理，不构成任何投资建议！
【往期精彩】