verus-lang/verus

Verus 为 Rust 增加规范、证明和 ghost code，让开发者用 SMT 求解器静态验证实现满足前置条件、后置条件与不变量。它保留 Rust 的所有权与类型系统，同时把功能正确性要求提升到机器检查的逻辑层。代价是需要显式建模和证明工程，因此更适合安全关键组件、协议与底层库，而非无差别覆盖所有业务代码。