Le marteau-pilon，Saint-Chamond锻造厂和钢铁厂，Joseph-Fortuné LAYRAUD，1889

关于

Creusot 是一个 演绎验证器，用于Rust代码。它验证您的代码不会发生panic、溢出和断言失败。通过添加注释，您可以进一步验证您的代码是否执行了 正确 的操作。

Creusot通过将Rust代码翻译为WhyML（Why3的验证和规范语言Why3）来工作。用户可以利用Why3的全部功能（半）自动执行验证条件！

有关技术细节，请参阅 ARCHITECTURE.md。

帮助和讨论

如果您需要使用Creusot的帮助或想要讨论，您可以在 讨论论坛 上发布帖子或加入我们的 Zulip聊天！

引用Creusot

如果您想在学术环境中引用Creusot，我们鼓励您使用我们的 ICFEM'22出版物。

验证示例

要了解使用Creusot验证程序的过程，我们鼓励您查看我们的部分测试套件

• 将向量清零
• 在向量和中二分搜索
• 对向量进行排序
• IterMut
• 规范化If-Then-Else表达式

更多示例请见 creusot/tests/should_succeed。

使用Creusot构建的项目

• CreuSAT 是一个用 Rust 编写的经过验证的 SAT 求解器，并通过 Creusot 进行了验证。它真正将工具推到了极限，让人对“实战使用”有了直观的了解。
• 还有另一个大型项目正在进行中 :)

作为用户安装 Creusot

1. 安装 rustup，以获取合适的 Rust 工具链
2. 获取 opam，OCaml 的包管理器
3. 克隆 creusot 仓库，然后 将工作目录移动到 creusot 以进行后续设置。

   $ git clone https://github.com/creusot-rs/creusot
   $ cd creusot
   

4. 设置 Why3 和 Alt-Ergo。创建一个包含 why3 和 alt-ergo 的本地 opam 切换

   $ opam switch create -y . ocaml.4.14.1
   $ eval $(opam env)
   

   这将在一个本地的 _opam 目录中构建 why3、alt-ergo 以及它们的 OCaml 依赖。
5. 构建 Creusot

   $ cargo install --path creusot-rustc
   $ cargo install --path cargo-creusot
   

   这将构建 cargo-creusot 和 creusot-rustc 可执行文件，并将它们放置在 ~/.cargo/bin 中。
6. 设置 Creusot

   $ cargo creusot setup install
   

   这将下载额外的求解器（Z3、CVC4、CVC5）并配置 Why3 以使用它们。

升级 Creusot

1. 进入之前用于安装 Creusot 的克隆的 Creusot git 仓库
2. 更新 Creusot 的源代码

   $ git pull
   

3. 如果需要，升级 Why3 和 Alt-Ergo

   $ eval $(opam env)
   $ opam update
   $ opam install .
   

4. 重新构建和重新安装 Creusot

   $ cargo install --path creusot-rustc
   $ cargo install --path cargo-creusot
   

5. 重新运行 Creusot 的设置

   $ cargo creusot setup install
   

使用 Creusot 和 Why3 进行验证

查看 指南。

在 Creusot 上进行黑客攻击

查看 HACKING.md 了解 Creusot 代码库的开发者工作流程。