Aeneas

Aegis 是一个面向真实实现验证的新基准，其构建流程为：先写出安全的 Rust 解法，再借助 Aeneas 翻译成 Lean，随后生成规约，最后为每条冻结的语句标注经内核检查的证明或反证。

Aeneas 是一个将 Rust 程序转化为 Lean 函数式模型的工具，由微软研究院等机构开发，用于对真实系统代码进行形式化推理。