防锈验证工具 这是支持Rust程序的静态和动态验证的工具/库的集合。 我们将静态验证(形式验证)和动态验证(测试)视为同一活动的两个部分,因此这些工具可用于两种形式的验证。 使用模糊测试/属性测试库进行动态验证。 使用符号执行引擎的静态验证。 我们的目标是在不久的将来添加其他后端。 此外,如果您要移植供Rust使用的验证工具,的工具如何工作。 (特别是,我们描述了如何生成可与基于LLVM的验证工具一起使用的LLVM位代码文件。) 工具和库 verification-annotations板条箱:用于在创建符号值的FFI层 propverify crate:用于静态验证工具的库的实现。 scripts/cargo-verify :用于编译包装箱并验证主要/测试或模糊主要/测试的工具。 (使用--backend标志选择。) compatibility-test测试箱:可以使用原始