1. 参与对开鸿操作系统的形式化验证，利用定理证明、模型检测、静态分析等多种技术对LiteOS-M/A或OpenHarmony的核心API作形式化验证，发现代码缺陷、在硬件中复现并整改，确保其功能正确性、安全性、可用性。
2. 开发形式化验证工具，利用AI领域最新发展动态提高证明效率，验证操作系统源码。
3. 利用形式化技术验证软总线协议，赋能高质量软总线标准规约的实现。
1. 熟悉嵌入式操作系统（RTOS/微内核）的开发与调试，了解对应的安全需求 2. 有应用形式化方法对较大复杂代码库/协议作形式化验证的经验。
