【实习】形式化验证算法实习生

职位概述
我们正在寻找一位对软件可靠性与形式化验证充满热情的实习生，你将深度应用数学逻辑、交互式定理证明（如Coq）、代码自动验证（如Dafny）及编程语言理论，参与构建严格形式化验证的软件基础架构，确保系统的正确性与安全性。

核心职责
参与形式化验证项目，使用Coq,等工具对软件系统进行数学建模与机器验证。
编写、维护并优化形式化验证脚本，覆盖从需求到实现的完整生命周期。
与跨职能团队协作（深度学习，大语言模型），将理论成果（如操作语义、Hoare逻辑、静态类型系统）应用于实际系统的设计与优化。
开展编程语言理论基础研究，探索类型系统、语义模型等前沿方向。

职位要求
计算机科学、数学、逻辑学或相关领域本科及以上学历。
熟悉函数式编程范式及逻辑基础（如命题逻辑、谓词逻辑）。
了解形式化验证工具链（如Coq、Isabelle/HOL等）。
掌握编程语言核心理论（如操作语义、类型系统）或算法验证方法。
具备较强的数学抽象与逻辑推理能力，能独立解决复杂问题。