编程智能体能否用 Lean 4 形式化验证真实 Rust 代码的行为？

i5h 基准测试 每道题都对应某个开源 Rust 应用的一项性质：它的安全相关逻辑（访问控制、输入校验、解析）被移植到 i5h，再提取成 Lean 4。智能体会拿到移植后的 Rust 代码、提取出的 Lean 代码以及一份规格说明，然后证明该性质成立。点击任意题目，可以查看上游原版 Rust、移植版本、两者如何互相校验、Lean 代码，以及各模型写出的证明。 仍在进行中 本基准测试还在测评中。下面的结果是阶段性快照：并非每个模型都跑完了所有题目，数字后续还会变化。 ## i5h 是什么 i5h 是一个 Rust Web 框架，它的应用逻辑可以在 Lean 4 中证明正确。 1. **R