精选理由
形式化验证从学术走向商业云，做云安全或高合规性系统的团队值得关注——数学证明比测试更可靠，AWS已经把它落地了。
亚马逊AWS宣布其Nitro隔离引擎（Nitro Isolation Engine）已在Graviton5实例上正式商用，成为首个部署在商业云中的形式化验证的虚拟机监控器。该引擎通过33万行机器检查的数学证明来确保安全隔离，消除了传统软件漏洞的风险。这一突破意味着云租户可以依赖数学保证而非仅靠测试来获得隔离安全性，对高安全需求的行业（如金融、医疗）尤为重要。
AI 翻译 · 中文
亚马逊AWS宣布其Nitro隔离引擎（Nitro Isolation Engine）已在Graviton5实例上正式商用，成为首个部署在商业云中的形式化验证的虚拟机监控器。该引擎通过33万行机器检查的数学证明来确保安全隔离，消除了传统软件漏洞的风险。这一突破意味着云租户可以依赖数学保证而非仅靠测试来获得隔离安全性，对高安全需求的行业（如金融、医疗）尤为重要。
The first formally verified hypervisor is now deployed in a commercial cloud. The Nitro Isolation Engine is generally available today on Graviton5, backed by 330,000 lines of machine-checked mathematics: https://t.co/P8H…