Vermilion 实验：为 Verus 实现精简 Lean 后端

Vermilion 是为 Rust 验证器 Verus 构建的实验性 Lean 后端，让带普通 Verus 规格的程序获得交互式证明和 Lean 数学库支持。它保留 Verus 现有的验证条件翻译，只改变证明方式，示例 Rust 代码与 Lean 证明已收录在开源仓库中。