マイクロソフトは、WindowsやAzureなどの製品で使用されるSymCrypt暗号技術プロバイダーで、Rustで書かれた新しいアルゴリズムのセキュリティを形式検証によって強化している。このアプローチは、従来のテストや検証手法を超えて、暗号技術コードの小さなエラーが大きなセキュリティの脆弱性につながるのを防ぐことを目指している。特に、ポストクォンタム暗号技術のような複雑なアルゴリズムでは、この手法が重要である。

検証プロセスは、公開されている規格（NIST、IETF RFC）をLean形式証明フレームワークで実行可能な仕様に変換することから始まる。その後、AeneasツールがRustコードをLeanモデルに変換し、開発者が書いたパフォーマンス指向のRustコードが数学的な仕様に適合していることを証明することを可能にする。このことで、Rustのメモリセキュリティエラーを防ぎながら、Lean証明が機能的な正確性を保証する。

この方法では、生産コードの複雑さ（SIMD命令、Architecture固有の最適化など）を維持しながら検証を行うことが可能である。また、AIエージェントは、証明の書き込みや維持プロセスを自動化することで、検証の拡張性を高める。開発者は、自動生成されたパネルを通じて検証された関数、前提条件、仮定を簡単に追跡することができる。

このシステムは、SHA-3やML-KEMのようなアルゴリズムのRust実装に対して完全な証明を提供し、SymCryptをWindowsのプレビューバージョンで使用することを可能にする。マイクロソフトは、AES-GCM、FrodoKEM、ML-DSAのようなさらに多くのRustベースのアルゴリズムをこの手法で検証し、WindowsやLinuxの生産バージョンに統合することを計画している。