在软件开发领域，代码的正确性至关重要。为了确保Rust编程语言写成的代码能够准确执行其规定的功能，Verus工具应运而生。开发者通过编写代码的规格说明，Verus工具便能静态地检查可执行的Rust代码是否总是满足这些规格说明，以保证代码在所有可能的执行过程中都是正确的。
静态验证的优势
与添加运行时检查不同，Verus依赖于强大的求解器来证明代码的正确性。目前，Verus支持Rust的一个子集，并且正在努力扩展这一范围。在某些情况下，它甚至允许开发者超越标准Rust类型系统，静态检查例如原始指针操作等复杂代码的正确性。
开发现状
Verus仍处于活跃开发阶段。其功能可能存在缺陷或尚未完善，文档也还不完整。如果想尝试使用Verus，开发者需要准备在Zulip上寻求帮助。
学习与贡献
想要在浏览器中尝试Verus，可以访问Verus Playground。对于更深入的开发，可以按照安装说明进行操作。然后，可以开始阅读以下文档，从教程和参考资料入手。
Verus的文档资源还在完善中，包括教程、参考资料等。开发者可以在GitHub上报告问题或开始讨论，或者加入Zulip进行更实时的讨论和寻求帮助。感谢大家使用并为Verus做出贡献！
社区互动
GitHub讨论区用于功能请求和关于即将推出的功能的更开放的讨论，而GitHub问题区则专门用于现有功能的可操作问题（错误）。如果有人认为某个问题应该是一个讨论（或相反），可以随时移动。
Verus欢迎大家的贡献！如果你想贡献代码，请查看《为Verus贡献》中的提示。
Zulip的支持
Zulip为Verus提供了免费的托管服务。Zulip是一个开源的现代团队聊天应用，旨在保持实时和异步交流的有序。
