用 Rust、Lean 与 AI 代理验证 SymCrypt 加密实现

微软研究院介绍 SymCrypt 如何结合 Rust、Aeneas 与 Lean，对生产级密码算法从标准到代码进行形式化验证。首批发布内容包括 SHA-3 和后量子算法 ML-KEM 的验证代码、规格、性质与证明，AI 代理用于扩展可独立检查的证明自动化。