任职要求：
1. 精通Coq交互式定理证明器

熟练掌握 Coq的使用，具备构建形式化模型、编写证明脚本和管理验证工程的能力；

有使用该工具完成过形式化验证项目（如语言语义、协议、算法或系统组件验证）的实际经验。

2. 扎实的形式化方法基础知识

理解形式语义（操作语义、指称语义等）、逻辑系统（高阶逻辑、类型理论）、程序验证（Hoare logic、分离逻辑等）的基本原理；

能够将系统（程序）行为抽象为可验证的数学模型，并设计合理的验证规范与不变式。

3. 工程化能力与协作意识

熟悉版本控制（Git）和持续集成，能维护结构清晰、可复用、可维护的证明代码库；

具备良好的文档习惯，能清晰撰写技术说明与证明策略。

4. 加分项（非必需但优先）：

了解实时系统的基本概念（如任务调度、中断处理、时间约束等）；

有操作系统组件（如调度器、内存管理、IPC）的形式化验证经验；

熟悉相关辅助验证工具（如 Why3、Frama-C、VST等）；

计算机科学、软件工程、数学或相关领域本科及以上学历。