Verus: Verified Rust for low-level systems code
a year ago
- #static-analysis
- #Rust
- #formal-verification
- Verus 是一个通过静态检查验证 Rust 代码正确性的工具
- 它使用开发者编写的规范与求解器来证明代码正确性
- 当前支持 Rust 语言子集，未来计划扩展功能
- 可检查超出 Rust 类型系统范畴的操作（如原始指针操作）
- 处于积极开发阶段，部分功能可能不完善
- 通过 Zulip 提供社区支持与讨论平台
- 其出版物页面列出了相关研究论文和使用 Verus 的项目
- 提供浏览器版 Verus Playground 测试环境
- 文档包含教程、API 文档、并发代码指南等内容
- 提供示例代码、视频教程和练习案例展示实际应用
- GitHub 用于问题追踪和讨论，欢迎贡献代码
- Zulip 为 Verus 社区提供免费讨论平台托管
- Verus 徽标由 Johanna Polzin 设计，采用 CC BY 4.0 许可