访问官网
Github
文档
论文
Verus 是一个用于验证 Rust 代码正确性的工具。开发者编写代码应该做什么的规范，Verus 会静态检查可执行的 Rust 代码是否在所有可能的执行情况下都能满足这些规范。Verus 不是添加运行时检查，而是依靠强大的求解器来证明代码的正确性。Verus 目前支持 Rust 的一个子集（我们正在努力扩展），在某些情况下，它允许开发者超越标准 Rust 类型系统，静态检查例如操作原始指针等代码的正确性。
状态
Verus 正在积极开发中。功能可能会出现故障或缺失，文档也仍不完整。如果您想尝试 Verus，请做好准备在 💬 Zulip 上寻求帮助。
Verus 社区已发表了多篇研究论文，有多个行业和学术项目正在使用 Verus。您可以在我们的出版物和项目页面上找到列表。如果您正在使用 Verus，请考虑将您的项目添加到该页面（请参阅那里的说明）。
尝试 Verus
要在浏览器中尝试 Verus，请访问 Verus Playground。 如需更深入的开发，请按照我们的安装说明进行操作。 然后您可以深入研究下面的文档，从 📖 教程和参考 开始。
文档
我们正在编写的文档资源包括：
联系我们、报告问题和开始讨论
请在 GitHub 上报告问题或开始讨论，或者加入我们的 💬 Zulip 进行更实时的讨论和寻求帮助。感谢您使用和为 Verus 做出贡献！
我们使用 GitHub 讨论来处理功能请求和关于即将推出功能的更开放式对话，我们保留 GitHub 问题用于现有功能的可操作问题（错误）。不过别担心：如果我们认为某个问题应该是讨论（或反之），我们随时可以移动它。
我们欢迎贡献！如果您想贡献代码，请查看 为 Verus 做贡献 中的提示。
Zulip 为 Verus 提供免费托管赞助。Zulip 是一款开源的现代团队聊天应用，旨在保持实时和异步对话的有序组织。
