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

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

在形式化验证和原生保证方向，望安科技当做国内较早布局相干技术的革新公司，在本届大会中经过四场论坛汇报集中展示其研发进展、工具链体系与实际工程经验，使更多产业参与者熟悉形式化验证怎样业务于基本软件可信、保证内核构建还相干键系统的研发。

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

在另一场汇报中，赵永望教授作《操作系统形式化验证：现状与挑战》汇报。操作系统的全体错误都或许引发系统崩溃或被攻击，作用整体保证与可靠性。常规“事后补丁式”保证方案往往治标不治本，无法避免缺陷反复呈现。鉴于原生保证理念，操作系统需求从架构策划开启就设立可信基本，而形式化验证正是达成这一目的的关键技术。经过数学化的规约描述与严格证明，可在研发早期发觉深层逻辑漏洞，确保系统调用、调度机制、权限治理等模块适合预设保证与功能需求。汇报对国内外探讨现状、关键技术难点另有工程化挑战做出了系统解析，为将来进展给予了方向。

望安科技形式化验证工程师王布阳作《鉴于Auto-active与交互式集成的L4线程治理形式化验证》汇报。汇报分享了团队经过围绕 L4 微内核的关键机制——线程治理，开展了系统的形式化规约与验证探讨。在验证流程中，团队将交互式验证与 Auto-active 方法结合，不但提升了验证自动化程度，此外效减少了人工证明工作量。

望安科技技术副总裁张峰作《以形式化方法构建基本软件原生保证》汇报。原生保证不是常规保证加固的延伸，而是从产品规划、需求策划、架构建模到研发验证的全生命周期保证体系。其核心是以形式化方法为支撑，经过抽象建模、符号解析、自动化证明等手段验证关键模块的策划正确性，达成保证需求、策划逻辑与系统行为的严格一致。张峰详细展示了望安科技怎样经过形式化验证技术和“穹道”原生保证系统作用于内核、系统调用、调度器、内存治理和关键库函数，协助公司从根本上消除深层策划缺陷，保证产品长期业务价值，确实构建“先天可信、内生保证”的基本软件。

2025 CCF 我国软件大会的胜利举办为产业给予了思想沟通与技术前瞻的系统。当做赞助单位和深度参与者，望安科技不但展示了技术实力，也促进了形式化验证、原生保证等领域的学术沟通与产业协作。多位与会专家觉得，形式化验证正在从学术工具走向工程体系，而“原生保证”正变成基本软件建设的关键动向。望安科技在本届大会上集中展示的实践案例，为产业给予了可参考的工程路径，也促进相干技术在更多场景中的应用讨论。

(责任编辑：汽车)