Verus：用形式化验证写出可证明正确的 Rust
Amazon Science 文章介绍开源自动化程序验证器 Verus：针对 Rust 代码，用形式化数学规格描述应有行为，并机械检查对所有可能输入是否成立，覆盖传统测试容易漏掉的边界情况。作者 Bryan Parno；文中日期为 2026-08-31。
开发者在源码里用接近 Rust 的语法直接写前置条件（requires）与后置条件（ensures）；普通 rustc 会忽略这些注解，因此同一份代码可同时服务已验证与未验证工程。验证失败时反馈多为源码级、类 Rust 报错，常见交互反馈可在 1 秒内。Verus 还可对 unsafe 代码块以及带自定义锁不变量的并发代码做机器检查，把安全保证重新建立起来。Amazon 已将其用于 Nitro Isolation Engine 等关键基础设施中的关键原语；开源侧用例包括 Vest（二进制格式解析/序列化及证明）、Verdict（可配置策略的 x.509 证书校验）、CapybaraKV（持久内存日志崩溃安全）、Atmosphere 微内核、Anvil（Kubernetes 控制器正确性与 liveness）、CortenMM 等。与 Miri 不同：Miri 侧重已执行路径上的 UB 检查，Verus 则相对开发者给出的规格做全输入证明。
原文链接：https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus
sofka：Rust 实现的 Kubernetes TUI（k9s 替代）
sofka 是用 Rust 写的 Kubernetes 终端界面，基于 kube-rs 与 ratatui，从设计起就全链路异步，UI 不会被集群请求卡住。项目站点为 sofka.rs，仓库约 1.1k star；协议 MIT/Apache-2.0，提供 macOS/Linux 预编译二进制。
核心差异是单一通用对象流水线，而不是按资源种类各写一套渲染：内置资源与 CRD 都能用，常见 kind 有内置列，其余回退 NAME/AGE，进入 CRD 可继续浏览其实例。内置 Flux CD 操作（挂起/恢复/协调）与 Argo CD 相关操作，通过原生 API patch 完成，不依赖 flux/argocd 二进制；另有自行解码 Helm release Secret 的检查器。X 打开基于证据的故障说明视图（无外部 AI 服务）；支持批量标记删除/kill/Flux 动作、后台 port-forward、生产环境删除护栏与只读模式，以及多套皮肤。
原文链接：https://github.com/nklmilojevic/sofka/
Rust + Vulkan 流体模拟：100 万粒子约 180 FPS
作者展示用 Rust 与 Vulkan 做的实时 GPU 流体模拟学习项目。实现 Divergence-Free SPH（DFSPH），邻居搜索使用 GPU octree；在 AMD 6800XT 上约 100 万粒子、约 180 FPS。仓库描述为 GPU fluid simulation in Rust、Vulkan、Slang；附有演示视频。
原文链接：https://github.com/MarcVivas/fluid-simulation
rusty-broom：清理长期未动项目的构建产物
rusty-broom 是用于释放磁盘的 CLI/TUI：扫描并清理长时间未开发项目中的构建产物（如 target、node_modules、.venv、build、Pods 等）。项目“新旧”按源码文件 mtime 判断，而不是按产物时间；删除前只针对 git check-ignore 认为被忽略的路径。支持 Rust、Python、Node、Java、Go、.NET、CMake、Swift 等；提供交互 TUI 与 JSON 输出。可通过 cargo install rusty-broom 安装，并支持按时间阈值扫描、--dry-run 预览清理。
原文链接：https://github.com/oriontvv/rusty-broom
From Rust中文社区 Mike
社区学习交流平台订阅：
评论区
写评论还没有评论