Microsoftは、ML-KEMおよびSHA-3のRust実装に対する形式仕様と証明を含む、その暗号化ライブラリであるSymCryptのブランチをオープンソースとして公開しました。このリリースは、本番環境のアルゴリズムを安全なRustで記述し、Aeneasツールチェーンを使用してLeanモデル（標準から派生）に対して検証するという手法を示しています。

  • このアプローチでは、Aeneasを使用してRustの中層表現を純粋なLeanモデルに変換し、Rustの所有権ルールを活用してメモリの安全性に関する推論を簡素化します。
  • 形式仕様は、NISTやIETF RFCなどの公開標準に密接に合わせるように設計されており、公式ベクトルに対する実行可能なテストや行ごとの人間によるレビューを可能にします。
  • オープンソース化されたブランチには、Windows Insiderビルズで現在使用されているML-KEMおよびSHA-3のコードに対する完全な証明が含まれており、このワークフローをAES-GCM、FrodoKEM、ML-DSAに拡張する計画があります。

この手法は、Rustのメモリ安全性の保証とLeanによる機能的正しさの証明を組み合わせて2層の信頼性を提供し、本番環境の暗号化アルゴリズムに対する形式検証のスケーラビリティを目指しています。