Creusot 帮助您证明您的 Rust 代码是正确的

Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889 Creusot 关于 Creusot 是 Rust 代码的演绎验证器。它验证您的代码是否安全，不会出现恐慌、溢出和断言失败。通过添加注释，您可以进一步验证您的代码是否正确执行操作。 Creusot 的工作原理是将 Rust 代码翻译为 Coma，Coma 是 Why3 平台的中间验证语言。然后，用户可以充分利用 Why3 的​​全部功能（半）自动解除验证条件！有关技术细节，请参阅 ARCHITECTURE.md。帮助和讨论 如果您需要使用 Creusot 的帮助或想要讨论，您可以在讨论论坛上发帖或加入我们的 Zulip 聊天！引用 Creusot 如果您想在学术环境中引用 Creusot，我们鼓励您使用我们的 ICFEM'22 出版物 。验证示例 为了了解使用 Creusot 验证程序的情况，我们鼓励您查看我们的一些测试套件： 将向量归零 对向量进行二分搜索 对向量进行排序 IterMut 规范化 If-Then-Else 表达式 更多示例可以在 Examples 和 tests/should_succeed 中找到。使用 Creusot 构建的项目 CreuSAT 是一个用 Rust 编写并经过 Creusot 验证的经过验证的 SAT 求解器。它确实将该工具推向了极限，并让我们了解了“愤怒时使用”是什么样子。另一个大项目正在进行中:) 以用户身份安装 Creusot 安装 rustup ，以获得合适的 Rust 工具链 获取 opam ，OCaml 的包管理器 克隆 creusot 存储库，然后移至 creusot 目录。 git clone https://github.com/creusot-rs/creusot cd creusot Install Creusot : ./INSTALL 检查安装是否成功：cargo creusot --help 请参阅 Creusot 指南：安装了解更多详细信息。升级 Creusot 输入之前用于安装 Creusot 的克隆 Creusot git 存储库 更新 Creusot 的源代码： git pull 更新 opam 的软件包列表： opam update 重新安装 Creusot： ./INSTALL 对 Creusot 的黑客攻击 有关对 Creusot 代码库进行黑客攻击的开发人员工作流程的信息，请参阅 CONTRIBUTING.md。