微软用AI Agent验证Rust密码学代码
Microsoft Research · rss · 2026-07-14
微软研究院发文介绍如何利用 Rust、Lean、Aeneas 和 AI agents 来扩展生产级密码学算法的形式化验证。 - **背景**：密码学代码对安全性要求极高，传统测试不足。微软在 SymCrypt（Windows 和 Azure 使用的加密库）中用安全 Rust 重写算法，并用 Lean 框架进行形式化验证。 - **方法**：使用 Aeneas 工具将 Rust 代码翻译为纯 Lean 模型，证明其符合标准规范。AI agents 被引入来编写可独立验证的证明，从而扩展自动化规模。 - **进展**：已开源包含 SHA-3 和 ML-KEM（后量子密码）完整证明的代码分支，正扩展至 AES-GCM 等更多算法。 - **优势**：软件工程师可继续编写高性能 Rust 代码，验证工程师则在生成的 Lean 模型上工作，互不干扰。