Isabelle/HOL：Nitro分離エンジンの背後にある証明支援系

AWSが2025年re:Inventで、顧客データの安全性を確保しつつリソースを提供するソフトウェアモジュール「Nitro分離エンジン」を発表した。AWSは証明支援系Isabelle/HOLを用いて同エンジンの正確性とセキュリティ保証を形式的に検証し、初の形式的検証済みクラウドハイパーバイザーとして新基準を確立した。