creusot:Rust代码的演绎验证。 (半)自动证明您的代码符合您的规范! 源码

关于 Creusot是用于对Rust代码进行演绎验证的工具。 它允许您用规范,不变式和断言来注释代码,然后进行形式检查,并返回满足您的规范的证明。 Creusot的工作原理是将Rust代码转换为WhyML的验证和规范语言 。 然后,用户可以利用Why3的全部功能来(半)自动释放验证条件! 注意:我正在博士学位论文的背景下进行开发,软件质量是相当的。 正在安装 使用rustup安装Rust以管理工具链 克隆存储库 安装Rust编译器库: rustup component add rustc-dev (可选,推荐)安装Rust编译器源: rustup component add rustc-