Vermilion 开源实验将 Verus 的 Rust 验证条件接入 Lean/Mathlib，允许 AI agent 辅助交互式补证

Ilya Sergey 于 10 月 18 日发表 Vermilion 实验项目说明，公开把 Verus 的 Rust 验证条件从 SST 转换为 Lean proof obligations 的新后端：Lean tactics 与重建后的 SMT 证明先自动处理简单义务，复杂证明可复用 Mathlib、由人类或编码 agent 交互完成。merge-sort 示例报告 40 个 obligations 中 31 个自动验证、9 个交互完成；一个小型对照 suite 中 Vermilion 相对原生 Verus 约慢 16 倍。作者披露最初原型在 GPT Astra、Claude Fable 帮助下实现。项目目前并非基础化的完整 Rust verifier：SST 到证明义务的翻译可信性、Rust 全语义、并发与不安全内存操作仍未形式证明或覆盖。