【Rust日报】2026-09-13 Verus：用形式化验证写出可证明正确的 Rust
内容提要
亚马逊开源了 Rust 形式化验证器 Verus，通过 requires/ensures 规格机械检查所有输入，覆盖测试盲区，支持 unsafe 与并发代码，已用于 Nitro 等基础设施。此外还有 sofka（Rust 版 k9s 替代）、Rust+Vulkan 百万粒子流体模拟（约 180 FPS）和清理闲置项目构建产物的 rusty-broom 等工具。
延伸解读
Verus 与 Miri 的定位差异
文章指出，Miri 侧重检查已执行路径上的未定义行为，而 Verus 则针对开发者给出的形式化规格，证明对所有可能输入都成立。这意味着 Verus 能覆盖测试难以触及的边界情况，但前提是规格本身正确。两者并非替代关系，而是互补：Miri 帮助发现运行时 UB，Verus 提供全输入范围的数学保证。
Verus 在工业与开源中的落地
Verus 已被 Amazon 用于 Nitro Isolation Engine 等关键基础设施中的关键原语，开源侧也有 Vest、Verdict、CapybaraKV、Atmosphere 微内核、Anvil、CortenMM 等用例。这些案例覆盖二进制解析、证书校验、持久内存日志崩溃安全、Kubernetes 控制器正确性与 liveness 等场景，表明形式化验证正逐步进入实际系统开发。
sofka 的设计取舍与适用场景
sofka 采用单一通用对象流水线，而非按资源种类分别渲染，因此内置资源与 CRD 都能统一处理。它基于 kube-rs 与 ratatui，全链路异步，UI 不会被集群请求阻塞。内置 Flux CD 与 Argo CD 操作通过原生 API patch 完成，不依赖外部二进制。适合需要轻量、快速且支持 CRD 的 Kubernetes 终端管理场景。
rusty-broom 的清理逻辑与安全边界
rusty-broom 按源码文件 mtime 判断项目新旧，而非构建产物时间，并只删除 git check-ignore 认为被忽略的路径。这降低了误删风险，同时支持 Rust、Python、Node 等多种生态。提供 --dry-run 预览和交互 TUI，适合在磁盘空间紧张时安全清理长期未动项目的构建产物。
Q&A
Verus 是什么？它如何帮助写出可证明正确的 Rust 代码？
Verus 是亚马逊开源的一个针对 Rust 的自动化程序验证器。它允许开发者在源码中用类似 Rust 的语法编写前置条件（requires）和后置条件（ensures）等数学规格，然后机械地检查这些规格是否对所有可能的输入都成立，从而覆盖传统测试容易遗漏的边界情况。普通 rustc 会忽略这些注解，因此同一份代码可以同时用于已验证和未验证的工程。
Verus 和 Miri 有什么区别？
Miri 侧重于检查已执行路径上的未定义行为（UB），而 Verus 则是相对于开发者给出的规格，对所有可能的输入进行全输入证明。
Verus 能处理 unsafe 代码和并发代码吗？
可以。Verus 能够对 unsafe 代码块以及带有自定义锁不变量的并发代码进行机器检查，从而重新建立安全保证。
sofka 是什么？它和 k9s 有什么不同？
sofka 是一个用 Rust 实现的 Kubernetes 终端界面（TUI），被视为 k9s 的替代品。它基于 kube-rs 和 ratatui，全链路异步，UI 不会被集群请求卡住。其核心差异是采用单一通用对象流水线，而不是按资源种类各写一套渲染，因此内置资源和 CRD 都能用。此外，它还内置了 Flux CD 和 Argo CD 操作，支持批量操作、后台 port-forward、生产环境删除护栏和只读模式等。
rusty-broom 是做什么的？它如何判断项目是否“老旧”？
rusty-broom 是一个用于释放磁盘空间的 CLI/TUI 工具，它可以扫描并清理长时间未开发项目中的构建产物（如 target、node_modules、.venv、build、Pods 等）。它根据源码文件的修改时间（mtime）来判断项目的新旧，而不是根据构建产物的时间。删除前只针对 git check-ignore 认为被忽略的路径，并支持 --dry-run 预览清理。
Rust + Vulkan 流体模拟的性能如何？
作者展示的用 Rust 和 Vulkan 实现的实时 GPU 流体模拟项目，在 AMD 6800XT 上运行约 100 万粒子时能达到约 180 FPS。该项目使用 Divergence-Free SPH（DFSPH）算法，邻居搜索使用 GPU octree。
