所谓形式化验证，是指从数学上完备地证明或验证电路的实现方案是否确实实现了电路设计所描述的功能。
形式验证方法分为等价性验证、模型检验和定理证明等。
形式化验证技术是彻底解决复杂系统设计与实现安全的技术手段，一般分为规约层、设计层、实现层三个层次，以及模型检测和数学证明两种实现方法。汽车及物联网产业界高级别安全认证强制要求对操作系统进行形式化证明（如国际上权威的Common Criteria认证，CC 4+以上要求形式化证明）。由于微内核代码规模与安全边界方面（如Linux内核中有大量驱动，驱动在适配芯片的过程中是大概率需要修改的。一旦驱动修改，整个内核都要重新验证，相比之下微内核驱动与服务多在用户空间，安全边界清晰）的优势，操作系统形式化方法绝大部分都与安全微内核技术相结合满足高安全要求。
目前，我们已经拥有C与Rust两套形式化验证工具，并且在Computers and Security (2020) 91 全球计算机安全顶级期刊发表关于形式化验证的高质量论文
《Automatic kernel code synthesis and verification》，在形式化验证技术上，我也取得了多项专利，并且针对自有产品Nebula、V-Trust、T-Hyper
在关键逻辑上进行了形式化验证。未来我们会加紧研究步伐，在形式化验证技术上不断取得卓越成就，为国家和社会创造有利价值。
1. 论文：《Automatic kernel code synthesis and verification》
Computers and Security (2020) 91 全球计算机安全顶级期刊 SCI检索 影响因子 3.0，研究内容：OS内核自动形式化证明，RISCV平台实践。
2.专利：软件验证方法、装置、计算机设备和存储介质【201910480992.5】
