一句话：提出 Varies，通过状态化验证 Harness 合成与反馈驱动调度，使 BMC 能高效检测 Rust 库中的不健全性缺陷。
Rust 的编译期安全保证可被库中 unsafe 代码引入的不健全性破坏。有界模型检测（BMC）虽可用于检测此类缺陷，但人工构造验证 harness 繁琐，且许多不健全性只在特定程序状态下触发，单一 harness 易遗漏。Varies 将检测建模为 harness 合成与预算感知验证的联合问题：为每个目标 API 构造种子 harness，通过变异器注入扩展为派生 harness，形成推导树；再利用反馈驱动剪枝调度验证。基准中，Varies 在更多 crate 上发现目标 API 缺陷且误报率低；在 crates.io 热门库中发现 10 个 crate 的未知不健全性，6 个获维护者确认。
Rust provides strong compile-time safety guarantees, but unsafe code in real-world libraries can still introduce unsoundness bugs that may undermine this guarantee. Compared with prior work, bounded model checking (BMC) offers a promising direction by adapting formal verification to unsoundness detection. In practice, however, BMC requires harnesses that are tedious to construct, and many unsoundness bugs arise only under specific program states that a single harness may miss. To this end, we propose Varies, a BMC-based framework that treats unsoundness detection in Rust libraries as a joint problem of harness synthesis and budget-aware verification. During the synthesis stage, Varies builds seed harnesses for each target API and then expands them into derived harnesses through mutator injection. Over the resulting harness derivation tree, Varies applies feedback-driven pruning strategies to schedule verification efficiently. In our benchmark, Varies identifies defects involving target APIs in more evaluated crates than any baseline while maintaining a low false-positive rate. In a broader deployment on popular crates.io libraries, it identifies previously unknown unsoundness in 10 crates, with reports for 6 crates acknowledged by maintainers. The results indicate that stateful harness synthesis and feedback-driven scheduling can make BMC practical for targeted unsoundness detection in Rust libraries.
@inproceedings{paperbot12457,
title = {VARIES: Verification Harness Synthesis and Efficient Scheduling for Unsoundness Detection in Rust Libraries},
author = {Huan Li and Xing Hu and Xin Xia and Xinyu Wang},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3837450}
}