2025年度CCF-华为胡杨林基金-形式化专项于2025年7月5日发布申报课题方向指南，并同步开启申报。

本年度共6个产业课题方向：

1、基于大模型的可形式化证明代码生成

2、面向形式化验证的RUST通用借用演算中间语言技术

3、基于TLA⁺模型的设计与代码功能一致性检查技术

4、面向TypeScript语言的轻量级形式化分析

5、面向大规模代码的神经符号融合分析

6、AI增强大规模Trace的预测分析技术

产业课题主要针对产业典型问题，持续提升形式化技术的能力上界、降低业界应用相关技术的门槛和成本，创造产业价值，形成本基金的正循环。

开放课题不限定具体研究内容，主要资助具有前瞻性、前沿性、能为产业全面升级储备能力，实现关键基础技术底座自主、领先的相关课题。

至截止时2025年8月31日24:00，共收到项目申请书39份，其中产业课题申请14份，开放课题申请25份。

9月15日~9月22日，形式化专委会和华为各三位专家组成的技术委员会对项目申请进行了预审评分。

产业课题围绕课题相关性、研究背景匹配度、技术先进性及合理性、项目交付风险、交付件、可落地性六个维度分别打分；

开放课题围绕形式化技术/产业课题相关性、研究背景匹配度、技术先进性及合理性、研究计划、交付件、应用价值六个维度分别打分；

9月23日晚召开了技术委员会线上会议，对项目申请进行正式评审，采取同单位专家回避原则，在专家充分发表意见的基础上，以全员表决的方式确定最终资助项目。本次评审过程的所有信息均备案可查。

经技术委员会评审，最终确定本年度资助产业课题方向项目5个，开放课题项目5个。

按计划，本年度资助项目于2025年12月开题，2026年6月中期审视，2026年12月进行答辩结题。

10个资助项目信息如下：