/
新型验证框架 关键字列表
Isabelle/HOL：驱动Nitro隔离引擎背后的形式化证明工具
AWS在2025年re:Invent大会上发布了Nitro隔离引擎（NIE），并采用证明辅助工具Isabelle/HOL完成了其正确性与安全性的形式化验证，使NIE成为首个经过形式化验证的云虚拟机监控程序。文章详细介绍了Isabelle/HOL在表达能力、自动化程度、证明可读性和可扩展性方面的优势，以及其在NIE验证中的具体应用，包括分离逻辑实现与25万行证明代码的高效处理。
白皮书
京公网安备 11010802021500号
