用Verus开发经过数学证明的Rust代码

Verus是一款面向Rust的开源自动化程序验证工具，通过形式化数学规范对所有可能输入进行机械化校验，超越传统测试手段。开发者可直接在Rust源码中用类Rust语法标注前置/后置条件，实现秒级反馈，并支持AI辅助生成证明...