勒芒庞-圣沙蒙，锻造和钢铁厂，约瑟夫-富尔唐·莱拉乌德，1889年

关于

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

Creusot通过将Rust代码翻译成WhyML（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)
   

   这将为什么3、Alt-Ergo及其OCaml依赖项在一个本地的 _opam 目录中构建。
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上黑客开发

有关在Creusot代码库上进行黑客开发的开发生态信息，请参阅HACKING.md。