verus-lang/verus

[](https://verus-lang.github.io/verus/guide/getting_started.html) [](https://verus-lang.github.io/verus/guide/) [](https://verus-lang.github.io/verus/verusdoc/vstd/) [](https://verus-lang.zulipchat.com) # Verus 是一个用于验证 Rust 代码正确性的工具。 开发者编写代码应该实现的功能规范， 而 Verus 会静态检查可执行的 Rust 代码是否在所有可能的代码执行中 都满足这些规范。 Verus 不依赖运行时检查，而是依靠强大的求解器来 证明代码的正确性。Verus 目前支持 Rust 的一个子集（我们 正在努力扩展该子集），在某些情况下，它允许开发者超越 标准的 Rust 类型系统，静态地检查代码的 正确性，例如，处理原始指针的代码。  ## 状态 Verus 正在*积极开发中*。部分功能可能已损坏或缺失， 文档也尚未完善。如果你想尝试 Verus，请做好 在[💬 Zulip](https://verus-lang.zulipchat.com/)中寻求帮助的准备。 Verus 社区已发表多篇研究论文，并且有 许多工业界和学术界的项目正在使用 Verus。你可以在我们的 出版物与项目页面上找到相关列表。 如果你正在使用 Verus，请考虑将你的项目添加到该页面（请参阅那里的说明）。 ## 试用 Verus 要在浏览器中试用 Verus，请访问 [Verus Playground](https://play.verus-lang.org/)。 对于更复杂的开发，请遵循我们的[安装说明](INSTALL.md)。 然后你可以深入阅读以下文档，从 [📖 教程与参考](https://verus-lang.github.io/verus/guide/)开始。 我们还支持为你的 Verus 代码使用自动格式化工具（[verusfmt](https://github.com/verus-lang/verusfmt)）。 ## 文档 我们（正在编写中）的文档资源包括： * [📖 教程与参考](https://verus-lang.github.io/verus/guide/) * [📖 Verus 标准库的 API 文档](https://verus-lang.github.io/verus/verusdoc/vstd/) * [📖 验证并发代码的指南](https://verus-lang.github.io/verus/state_machines/) * [为 Verus 贡献代码](CONTRIBUTING.md) * 在 [crates.io](crates.io) 上发布 Verus 相关 crate 的[最佳实践](best-practices-for-publishing-verusverified-code-on-cratesio)。 * [Verus 许可证](LICENSE) * [Verus Logo](https://verus-lang.github.io/verus/verus/logo.html) ## Verus 使用示例 除了上述文档外，观看 Verus 的实际使用也会很有帮助。以下是一些入门参考。 * 使用 Verus 的[出版物和项目](https://verus-lang.github.io/verus/publications-and-projects/)。 * 为期一天的 Verus 教程的[视频、幻灯片和练习](https://verus-lang.github.io/event-sites/2024-sosp/)。 * 展示在小型、具体任务中使用 Verus 的[独立示例](https://github.com/secure-foundations/human-eval-verus/)。 * 演示各种 Verus 功能的[中小型示例](examples) * Verus 的[单元测试](source/rust_verify_test/tests)，包含 Verus 语法和功能的示例。

标签：Rust, 云安全监控, 代码正确性, 可视化界面, 定理证明, 底层系统, 形式化验证, 网络流量审计, 通知系统, 静态分析