GitHub - formal-land/coq-of-rust: Rust 的形式验证工具：检查你的程序的 100%执行情况🦀 以制作超级安全的应用程序！✈️ 🚀 ⚕️ 🏦

coq-of-rust 简介：用于 Rust 的形式验证工具，能检查程序 100%的执行情况以打造超安全应用。Rust 的类型系统虽能避免很多错误，但仍可能存在漏洞，而“coq-of-rust”可通过数学证明程序对所有输入都符合规范，提供形式验证服务，包括设计规范和证明，开发主要由 Aleph Zero 基金会资助。
主要内容：
- Example（示例）：核心是将 Rust 程序翻译为 Coq 证明系统，如一个简单的 Rust 函数fn add_one(x: u32) -> u32 { x + 1 }，经“coq-of-rust”翻译后在 Coq 中为Definition add_one (τ : list Ty.t) (α : list Value.t) : M :=...，并可在 Coq 中表达和验证代码规范。
- Workflow（工作流程）：典型工作流程为将 Rust 代码经“coq-of-rust”翻译为 Coq 代码，通过链接和模拟等步骤使其更适合形式验证，最后编写规范并证明 Rust 程序满足规范，从而几乎将漏洞降为零。
- Rationale（原理）：形式验证可预防关键软件中的所有错误，Rust 的类型系统虽有保障但测试不完备，形式验证可覆盖所有情况，“coq-of-rust”将 Rust 程序翻译为 Coq 以使其 100%安全。
- Prerequisites（前提条件）：需具备 Rust 和 Coq（参考 coq-of-rust.opam）。
- Installation and User Guide（安装和用户指南）：build 教程提供构建和安装指导，user 教程介绍命令行界面和支持的选项。
- Language features（语言特性）：在 Rust 的 THIR 中间表示层面工作，支持 99%的 Rust 示例，包括基本控制结构、循环、引用、闭包、恐慌处理、用户类型、 trait 定义和实现等。
- Contact（联系）：如需 Rust 代码库的形式验证服务，可联系 mailto:contact@formal.land，可应用于智能合约、数据库引擎等关键 Rust 项目。
- Alternative Projects（替代项目）：其他从事 Rust 形式验证的项目有 Aeneas、Hacspec v2、Creusot、Verus、Kani 等。
- Contributing（贡献）：是开源软件，欢迎提交 pull 请求或 issue 参与贡献，Rust 代码遵循 AGPL 许可证，Coq 库遵循 MIT 许可证，部分代码取自 Creusot 项目以实现特定功能。