在线 Rust 程序验证经常涉及复杂的形式化方法和多种后端工具，单独使用难度较大，效率受限。 Aeneas 是一个开源的 Rust 程序验证工具链，基于将 Rust MIR 转换为纯 Lambda 演算的思想，支持 F*、Coq、HOL4 和 Lean 等多个形式化验证后端，提供了系统化的程序验证方案。 它不仅能与 Charon 项目无缝协作，自动生成中间表示，还支持符号执行、借用检查等高级验证功能，适合对 Rust 代码进行高精度形式化验证的研究者和开发者。 主要功能： - 将 Rust MIR 自动转换为纯 Lambda 演算表达式； - 支持多种形式化验证后端：F*、Coq、HOL4、Lean； - 与 Charon 集成，自动生成中间代码并完成验证流程； - 提供符号执行和借用检查的形式化证明； - 支持 OCaml 构建环境，提供详细文档和测试用例； - 适配 Nix 环境，方便快速启动和验证。