推荐：Electrolysis - Rust 程序的正式验证工具

---

项目介绍

Electrolysis 是一款独特的工具，其目的是将 Rust 程序转换为 Lean 定义，以便在 Lean 这个形式证明器中进行正式验证。这个项目由 Kha 开发，不仅提供了一个新颖的代码验证方法，还伴随着一份硕士论文和详细的官方参考文档。

• 硕士论文：简单验证 Rust 程序：通过功能净化 - 论文 | 演示
• 官方文档：Kha.github.io/electrolysis
• 博客分享：Rust 的二分搜索实现的形式验证 - 文章

技术分析

Electrolysis 利用 Rust 夜间编译器的不稳定私有 API。由于 API 极度不稳定，因此需要特定版本的夜间编译器。项目配合 rustup.rs 使用，可以确保正确构建。一旦安装了 rustup，只需执行简单的命令即可构建项目，并导出所需代码用于 Lean 验证。

electrolysis$ rustup override add $(cat rust-nightly-version)
electrolysis$ rustup component add rust-src
electrolysis$ cargo run core

这会生成 core 模块（如 thys/core/config.toml 所示）所需的所有代码，并将其导出到 thys/core/generated.lean 文件，供后续的正确性证明使用。

应用场景

Electrolysis 在安全性要求极高的软件开发领域尤其有用，如操作系统、航空软件或金融系统。它允许开发者以数学保证的方式验证关键代码逻辑的正确性，避免潜在的安全漏洞和错误。

项目特点

1. 集成 Lean：利用 Lean 这种强大的形式证明语言来验证 Rust 代码。
2. 高度稳定：尽管依赖于 Rust 的不稳定的 API，但项目提供了明确的构建指南来确保兼容性。
3. 自动化生成：可自动生成 Lean 文件，简化了证明过程。
4. 案例丰富：包括对 Rust 二分搜索的完整形式验证，展示其实战价值。

Electrolysis 提供了一种创新的方法来增强 Rust 代码的可靠性，对于想要提升软件安全性的团队来说，这是一个不容忽视的工具。如果你是 Rust 或形式验证领域的爱好者，那么 Electrolysis 值得你一试。