Aeneas：Rust 程序验证工具链

Aeneas 是一个面向 Rust 程序的验证工具链，通过把 Rust 的 MIR 内部语言翻译为纯 lambda 演算来工作，设计上与 Charon 配合使用——Charon 把 Rust 程序编译为名为 LLBC 的中间表示，Aeneas 再消费该 .llbc 文件。它目前提供 F*、Coq、HOL4 和 Lean 四个后端，其中 Lean 与 HOL4 最为成熟，对偏函数和外在式终止证明有专门支持，并提供针对单子程序的专用策略。项目用 OCaml 编写（建议 OCaml 5），依赖 Charon 仓库的指定提交（可用 make setup-charon 自动设置，或软链本地版本）。用法是在目标 crate 内调用 Charon 生成 .llbc，再运行 ./bin/aeneas -backend {fstar|coq|lean|hol4} 处理该文件；Lean 后端生成的文件还需在 Lean 包中引入 Aeneas 依赖。当前限制：仅覆盖安全 Rust 的一个子集，嵌套循环内的 return 或跳到外层循环的 break/continue 尚不支持，以可变引用实例化泛型类型也不支持；unsafe 代码与并发的支持正在通过基于分离逻辑的推理推进。测试可用 make test 与 make verify 运行。