夜雨聆风伴随信息化、智能化战争加速演进，软件已经成为各类武器装备、指挥信息系统的核心中枢。普通软件的功能缺陷、隐性漏洞，在民用场景或许只会造成体验下降，而在国防军工领域，微小的代码隐患就可能引发装备失控、任务失败，甚至造成重大作战损失。在此背景下，高可信软件成为保障国防安全、实现科技自立自强的关键基础技术门类。系统厘清高可信软件的内涵价值，梳理国内领军科研工作者的创新成果，对标全球领域发展态势，对推动我国国防软件体系建设具有重要现实意义。
一、高可信软件的核心定义与技术特征
高可信软件，是面向安全关键场景构建，同时满足可靠性、安全性、实时性、可预测性、容错性与自主可控多重指标的软件系统。传统软件测试依靠大量用例模拟运行场景，只能尽可能发现已知问题，无法穷尽所有运行状态，难以证明系统不存在隐藏缺陷。高可信软件跳出单纯测试的思路，融合形式化验证、静态代码分析、系统容错设计、全生命周期可信管控等技术，以严格的数学逻辑为基础，对软件需求、架构、代码、运行行为开展系统性论证，从理论层面约束软件运行边界，确保软件只执行预设功能，杜绝非预期行为。
从可信指标维度来看，可靠性代表软件在规定环境、规定时长内持续完成既定任务的能力；安全性包含功能安全与网络安全，一方面规避软件故障引发硬件损毁、任务失效，另一方面抵御外部网络攻击、恶意代码入侵；实时性面向武器控制、航天测控等场景，保障指令响应时间稳定可控；容错性要求系统在局部组件异常、外部干扰条件下维持基本运行能力；可验证性则意味着软件全部设计逻辑、代码行为均可追溯、可复现、可检验。不同于通用软件追求功能丰富、迭代速度，高可信软件将“不出致命错误”放在首要目标，优先保障系统稳定与安全，广泛应用于航空航天控制系统、主战装备机载软件、联合作战指挥平台、无人集群控制系统等安全关键场景。
二、高可信软件在国防军工领域的重要意义
国防军工领域是高可信软件最重要的应用阵地，发展高可信软件技术，具备不可替代的战略意义。现代战争已经进入软件定义装备、数据驱动作战的新阶段，战机飞控系统、导弹制导程序、卫星星载软件、无人作战平台、战区指挥通信网络，全部依托大规模嵌入式软件运行。装备硬件性能再先进，一旦配套软件出现逻辑漏洞，整体作战能力便无从发挥。历史上多次出现过因软件时序错误、并发冲突、边界条件疏漏，导致运载火箭发射失利、军用飞行器任务终止的案例，直观体现军工软件可信性缺失带来的巨大风险。
首先，高可信软件是保障武器装备作战稳定性的底线支撑。战场环境复杂多变，电磁干扰、温度剧变、通信中断等极端条件随时出现，普通软件难以适应强扰动环境。依托高可信技术体系开发验证的装备软件，经过严格的形式化推演与极限场景验证，能够大幅降低随机故障概率，避免战时装备“非战损失效”，保障各类作战平台持续执行任务。其次，高可信软件是维护国防信息安全、防范供应链风险的核心屏障。当前大量商用通用软件工具存在未知后门与漏洞，如果国防关键系统过度依赖境外软件栈，极易埋下安全隐患。自主高可信软件技术能够实现核心代码、验证工具、开发环境全链条自主可控，摆脱外部技术桎梏，杜绝敌对势力通过软件漏洞实施网络渗透、远程操控。
与此同时，智能化作战体系的建设进一步放大了高可信软件的战略价值。无人作战集群、智能决策系统融合人工智能算法，软件规模与逻辑复杂度持续攀升，代码体量激增带来漏洞数量同步上涨。人工智能模型存在不确定性输出问题，传统测试手段难以评估智能软件的边界风险，必须依靠高可信理论搭建可信约束框架，限制智能系统的异常决策，防止无人装备脱离指挥、做出危险行动。长远来看，高可信软件技术水平，直接决定联合作战体系的韧性，是衡量一国国防信息化根基强弱的重要标尺，属于必须牢牢掌握在自己手中的基础核心技术。
三、王戟教授在高可信软件领域的核心贡献
2026年7月，中央宣传部授予国防科技大学王戟研究员“时代楷模”称号。作为我国高可信软件技术领域的主要开拓者，王戟深耕该领域三十余年，在理论创新、技术攻关、工程转化、人才培育多个维度取得系统性突破，推动我国高可信软件研究从一片空白走向跻身国际先进行列。早在上世纪末，国内尚未形成高可信软件统一研究方向，王戟敏锐预判信息化国防建设对可信软件的长远需求，率先提出高可信软件技术发展思路。2003年，他参与发表国内该领域首篇系统性学术论文，搭建起本土高可信软件工程理论雏形，随后率先开设研究生课程，把前沿理论引入高校人才培养体系，开辟了国内全新的科研赛道。
高可信软件的核心难点之一在于大规模并发程序的可信验证，航空航天、超算、指挥系统大量使用并行代码，多任务调度引发的隐性冲突极难排查。王戟带领团队瞄准这一世界性难题，深耕形式化方法与程序自动验证技术，持续攻关软件静态分析、模型检测、自动定理证明关键技术，研发一系列自主可控的软件可信分析验证工具链。这套工具相当于大国重器软件的“代码CT扫描仪”，能够深度挖掘传统测试无法发现的逻辑漏洞、并发缺陷，不需要海量测试用例，依靠数学推演完成代码正确性论证。相关成果先后应用于多项重大航空航天装备、主战武器软件评估，为关键装备软件安全稳定运行提供坚实技术保障，项目成果整体达到国际前列，部分指标实现国际领先，斩获军事科技进步一等奖等多项重要奖项。
科研道路上，王戟遭遇严重疾病打击，高位截肢后又长期依靠血液透析维持身体。巨大病痛没有阻挡科研报国的脚步，他以轮椅为战位，把病房作为临时办公室，持续牵头承担多项国家、军队重大基础科研项目，担任全军首个纯软件方向国防重大基础项目首席专家。在持续开展科研攻关的同时，他始终坚持立德树人，三十年间培养一百余名硕士、博士研究生，大量毕业生奔赴国防科研一线，充实高可信软件领域人才队伍。他牵头搭建全国性学术协作平台，凝聚起国内形式化方法与可信软件研究力量，推动分散的科研团队协同攻关，改变早期国内研究力量薄弱、分散孤立的局面。中宣部授予其时代楷模称号，既是表彰他身残志坚、为国铸盾的精神品格，也是充分肯定高可信软件技术对于国防现代化建设的重大战略价值，激励更多科研工作者投身基础软件自主创新事业。
四、国外高可信软件领域发展现状与态势
放眼全球，发达国家很早就意识到高可信软件对于国防、航空领域的战略价值，持续数十年投入资源布局相关研究，形成完整的理论体系、工具产品与工程标准。美国是高可信软件与形式化验证领域起步最早、投入力度最大的国家，国防高级研究计划局长期布局弹性软件、安全关键系统验证系列项目，推动形式化方法从实验室走向军工装备型号应用。相关研究成果陆续落地无人机、航空电子、太空系统，军方逐步将形式化可信验证纳入军用软件研制规范，在下一代无人作战平台、空中作战系统推广应用。同时，美国持续推动内存安全编程语言、标准化可信开发流程落地，减少因编程语言原生缺陷引入的软件漏洞，构建军用软件全生命周期可信管控体系。
欧洲各国聚焦航空、航天领域安全关键软件发展，多国联合开展大型航空安全研究计划，针对民航客机、军用飞行器机载软件制定严格的安全性审定标准，形成一套成熟的高可信软件工程规范。法国科研机构研发经过形式化验证的编译工具，从底层工具链层面保障程序转换过程不会引入错误，广泛应用于航天领域。欧洲军工企业持续推进可信软件工具商业化，形成成熟的工业级验证产品，支撑导弹、卫星、军用运输机等装备研发。
总体来看，国外先进国家已经完成高可信软件技术从理论研究向工程规模化应用的过渡，拥有成熟商业化验证工具、完善行业标准以及长期工程实践积累。同时也要看到，境外主流可信软件工具存在技术壁垒，对外提供版本存在功能限制，无法满足我国涉密军工装备研发需求，直接引进存在供应链安全隐患。海外相关技术发展也存在固有短板，大规模复杂系统、海量并发软件的高效验证依然存在瓶颈，面向人工智能融合场景的可信理论仍处于探索阶段，这也为我国实现技术赶超创造了机遇。
五、行业发展总结与未来展望
对比国际发展格局，经过多年持续攻关，特别是以王戟为代表的科研团队长期开拓，我国高可信软件领域已经建立自主理论框架，拥有自研验证工具，在航空航天、国防装备领域实现工程落地。但客观而言，产业层面依然存在短板，面向军工领域的标准化可信开发流程有待完善，工具链产业化程度不足，面向智能装备、无人集群的新一代高可信理论仍需持续深化。
现代大国科技竞争和军事对抗持续升级，软件可信性博弈将成为技术竞争的重要赛道。未来，持续推进高可信软件技术创新，一方面需要持续夯实基础理论，拓展形式化验证在大规模智能软件场景的适用能力；另一方面要推动科研成果工程化、标准化，构建适配我国军工体系的自主可信软件研发体系。同时持续培育科研人才梯队，传承科研工作者为国攻坚的精神，不断缩小与国际顶尖水平的差距，全面筑牢国防军工软件安全防线，为实现国防和军队现代化提供坚实的软件技术支撑。
