望安科技出席2025 CCF中國軟件大會，共話形式化驗證與原生安全

　　2025年11月28日—11月30日，2025 CCF 中國軟件大會在湖北省武漢國際會議中心圓滿舉辦。本屆大會以“軟件定義智能互聯新世界”為主題，全面展示我國軟件創新領域的前沿研究、先進工具鏈與產業實踐。大會邀請了12位中國科學院與中國工程院院士作特邀報告，并舉辦院士高峰論壇，同時組織了75個分論壇和活動，覆蓋軟件工程、系統軟件、形式化方法、工業場景落地及人才培養等多個關鍵領域。作為深度參與者，浙江望安科技有限公司在大會期間發布四場論壇報告，展示了其在“原生安全”和“形式化驗證”領域的最新研究成果和典型應用案例。

　　在形式化驗證和原生安全方向，望安科技作為國內較早布局相關技術的創新企業，在本屆大會中通過四場論壇報告集中展示其研發進展、工具鏈體系與實際工程經驗，使更多行業參與者了解形式化驗證如何服務于基礎軟件可信、安全內核構建以及關鍵系統的開發。

　　望安科技創始人、浙江大學博士生導師趙永望教授作《AI賦能的形式化驗證技術探索》報告。趙永望教授指出，AI/LLM 技術為形式化驗證應用帶來了新的機遇，并在報告中系統闡述了 AI 賦能形式化驗證的核心思路，同時分析其關鍵技術瓶頸與未來發展方向。

　　在另一場報告中，趙永望教授作《操作系統形式化驗證：現狀與挑戰》報告。操作系統的任何錯誤都可能引發系統崩潰或被攻擊，影響整體安全與可靠性。傳統“事后補丁式”安全方案往往治標不治本，無法避免缺陷反復出現。基于原生安全理念，操作系統需要從架構設計開始就建立可信基礎，而形式化驗證正是實現這一目標的關鍵技術。通過數學化的規約描述與嚴格證明，可在開發早期發現深層邏輯漏洞，確保系統調用、調度機制、權限管理等模塊符合預設安全與功能要求。報告對國內外研究現狀、關鍵技術難點以及工程化挑戰做出了系統分析，為未來發展提供了方向。

　　望安科技形式化驗證工程師王布陽作《基于Auto-active與交互式集成的L4線程管理形式化驗證》報告。報告分享了團隊通過圍繞 L4 微內核的關鍵機制——線程管理，開展了系統的形式化規約與驗證研究。在驗證過程中，團隊將交互式驗證與 Auto-active 方法結合，不僅提高了驗證自動化水平，還有效降低了人工證明工作量。