望安科技出席2025 CCF中国软件大会，共话形式化验证与原生安全

　　2025年11月28日—11月30日，2025 CCF 中国软件大会在湖北省武汉国际会议中心圆满举办。本届大会以“软件定义智能互联新世界”为主题，全面展示我国软件创新领域的前沿研究、先进工具链与产业实践。大会邀请了12位中国科学院与中国工程院院士作特邀报告，并举办院士高峰论坛，同时组织了75个分论坛和活动，覆盖软件工程、系统软件、形式化方法、工业场景落地及人才培养等多个关键领域。作为深度参与者，浙江望安科技有限公司在大会期间发布四场论坛报告，展示了其在“原生安全”和“形式化验证”领域的最新研究成果和典型应用案例。

　　在形式化验证和原生安全方向，望安科技作为国内较早布局相关技术的创新企业，在本届大会中通过四场论坛报告集中展示其研发进展、工具链体系与实际工程经验，使更多行业参与者了解形式化验证如何服务于基础软件可信、安全内核构建以及关键系统的开发。

　　望安科技创始人、浙江大学博士生导师赵永望教授作《AI赋能的形式化验证技术探索》报告。赵永望教授指出，AI/LLM 技术为形式化验证应用带来了新的机遇，并在报告中系统阐述了 AI 赋能形式化验证的核心思路，同时分析其关键技术瓶颈与未来发展方向。

　　在另一场报告中，赵永望教授作《操作系统形式化验证：现状与挑战》报告。操作系统的任何错误都可能引发系统崩溃或被攻击，影响整体安全与可靠性。传统“事后补丁式”安全方案往往治标不治本，无法避免缺陷反复出现。基于原生安全理念，操作系统需要从架构设计开始就建立可信基础，而形式化验证正是实现这一目标的关键技术。通过数学化的规约描述与严格证明，可在开发早期发现深层逻辑漏洞，确保系统调用、调度机制、权限管理等模块符合预设安全与功能要求。报告对国内外研究现状、关键技术难点以及工程化挑战做出了系统分析，为未来发展提供了方向。

　　望安科技形式化验证工程师王布阳作《基于Auto-active与交互式集成的L4线程管理形式化验证》报告。报告分享了团队通过围绕 L4 微内核的关键机制——线程管理，开展了系统的形式化规约与验证研究。在验证过程中，团队将交互式验证与 Auto-active 方法结合，不仅提高了验证自动化水平，还有效降低了人工证明工作量。