2025年11月28日—11月30日，2025 CCF中国软件大会在湖北省武汉国际会议中心圆满举办。作为本届大会的赞助单位，望安科技与华为、蚂蚁集团、百度、浪潮等企业共同支持大会顺利举办。大会期间，望安科技携四场论坛报告亮相，集中展示了团队在“原生安全”和“形式化验证”领域的最新研究成果与技术进展。
CCF ChinaSoft
CCF中国软件大会由全国软件与应用学术会议（NASAC）与全国形式化方法与应用会议（FMAC）有机组成，是目前国内软件科学与工程领域参会人数最多、影响范围最广的年度盛会。2025 CCF中国软件大会由中国计算机学会（CCF）主办，CCF软件工程专委会、系统软件专委会、形式化方法专委会、武汉大学承办，武汉大学计算机学院具体落实。大会协办单位包括武汉计算机软件工程学会、华中科技大学、中国地质大学（武汉）、武汉理工大学、华中师范大学等多所高校。
本届大会以“软件定义智能互联新世界”为主题，全面展示我国软件创新领域的前沿研究、先进工具链与产业实践。大会邀请了 12 位中国科学院与中国工程院院士作特邀报告，并举办院士高峰论坛，同时组织75 个论坛和活动，覆盖软件工程、系统软件、形式化方法、工业场景落地、人才培养等多项关键领域。望安科技在本届大会上发布四场论坛报告，展示了形式化验证技术在新时代复杂软件系统中的创新应用路径与真实产业价值。
论坛报告
报告一：AI赋能的形式化验证技术探索
望安科技创始人、浙江大学博士生导师赵永望教授作《AI赋能的形式化验证技术探索》报告。形式化验证通过数理逻辑方法对系统进行规约、开发与验证，已在航空航天等安全关键领域得到成熟应用，并逐步扩展到互联网领域，包括 Amazon、Google、Microsoft 等企业都在规模化使用。然而，面对大规模软件，形式化验证技术仍面临建模工作量大、形式化验证状态空间爆炸或证明规模巨大的难题。赵永望教授表明，AI/LLM技术为形式化验证应用带来了新的机遇，并在报告中系统阐述了 AI 赋能形式化验证的核心思路，同时分析其关键技术瓶颈与未来发展方向。
报告二：操作系统形式化验证：现状与挑战
赵永望教授作《操作系统形式化验证：现状与挑战》报告。操作系统作为计算机系统软件栈的底层核心，在航空、航天、轨道交通和无人系统等关键领域中起着不可替代的作用。赵永望教授在报告中指出，操作系统的任何错误都可能引发系统崩溃或被攻击，影响整体安全与可靠性。为此，形式化验证提供了一种严谨的方法，可帮助开发人员发现深层次缺陷，保障系统高安全性与可信性。报告系统梳理了操作系统形式化验证的背景意义、国内外研究现状及面临的技术挑战。
报告三：基于Auto-active与交互式集成的L4线程管理形式化验证
望安科技形式化验证工程师王布阳作《基于Auto-active与交互式集成的L4线程管理形式化验证》报告。第二代 L4 微内核在性能和灵活性上相比初代微内核有显著提升，并已在多个领域得到广泛应用。然而，操作系统内核的正确性与可靠性对系统稳定运行至关重要。报告分享了团队通过围绕 L4 微内核的关键机制——线程管理，开展了系统的形式化规约与验证研究。在验证过程中，团队将交互式验证与 Auto-active 方法结合，不仅提高了验证自动化水平，还有效降低了人工证明工作量。实践中发现源代码存在三处违反正确性与安全性的缺陷，并提出针对性的解决方案，为操作系统核心模块的安全可靠性提供了有力保障。
报告四：以形式化方法构建基础软件原生安全
望安科技技术副总裁张峰作《以形式化方法构建基础软件原生安全》报告。随着信息系统复杂性增加，操作系统内核及关键系统库的安全漏洞可能导致严重风险，传统测试手段已难以充分保障安全。报告介绍了形式化方法在安全验证中的核心技术，如模型检验、定理证明及安全策略建模，并探讨其在基础软件全生命周期中的应用，实现软件自身固有的安全能力。通过抽象建模、符号分析与自动化证明，对内核、系统调用和关键库函数进行形式化验证，可在早期发现潜在缺陷，确保安全策略严格执行。案例分析显示，形式化方法在提升安全性、降低漏洞风险及支持高可信基础软件构建方面具有显著效果。
定理证明竞赛
本届大会期间，望安科技创始人、浙江大学赵永望教授联合上海交通大学曹钦翔副教授、华为技术有限公司詹博华博士等学者共同举办了“第一届定理证明竞赛”，吸引了来自北大、中科院、港科大、南大、上海交大、哈工大、浙大、航天科工、蚂蚁集团及望安科技等高校和企业的选手参赛。竞赛围绕形式化验证与定理证明技术设计题目，兼顾理论基础、算法设计与工程实践，旨在激发国内学者对定理证明的兴趣与研究热情，为我国软硬件系统安全保障培养和储备新生力量。参赛者积极投入，竞赛过程紧张且充满挑战，最终圆满成功，赢得参赛者和行业专家的一致好评。
2025 CCF 中国软件大会的圆满举办，为软件行业带来了思想交锋与技术前瞻的宝贵机会。作为赞助单位及深度参与者，望安科技不仅展示了技术实力，也进一步推动了形式化验证、原生安全等关键领域的交流合作。未来，望安科技将继续加强核心技术研发，推进学术成果工程化落地，并携手产业与学术伙伴，共同推动我国软件产业的可信化发展，为数字社会安全建设贡献力量。