2026年7月20日至24日，由北京大学程序设计语言研究室主办的“C*开发与验证暑期学校”在北京大学中关新园1号楼集贤厅成功举行。本次暑期学校以“把证明写进C”为主题，聚焦C*语言这一“开发与证明一体化”的前沿技术，吸引了来自全国各地的学生、科研人员与业界系统开发者参与。

C*语言通过在C中嵌入形式化规约与证明，实现了代码中程序与证明的紧耦合，旨在显著降低系统软件形式化验证的门槛与成本。围绕这一核心理念，为期五天的课程设计了系统化的理论教学与实战演示。课程从C*语言概览与工具链入手，逐步深入到分离逻辑、验证条件生成、前向与后向证明策略等关键技术。每日下午三节连贯的课程，由浅入深地构建了参与者在程序验证领域的完整知识体系。

在为期五天的学习中，参与者不仅系统学习了如何编写带有证明的C代码，还亲身体验了验证条件自动生成与证明策略调试的完整流程。课程特别设置了每日理论讲解与现场Demo环节，并围绕PSI范式（证明-规约-实现）、证明自动化以及AI辅助自动证明智能体等前沿方向展开了深入研讨。7月24日，课程以一场题为“AI时代的编程语言设计”的Panel讨论圆满收官，为本次暑期学校画上了句号。