写完 unsafe 代码后如何验证它没有未定义行为？

结论：首选 Miri——Rust 官方的解释器，逐条执行 MIR 并检测未定义行为（悬垂指针、越界、数据竞争、违反栈式借用规则等）；辅以 Loom 验证并发算法、Kani 做模型检验，以及 AddressSanitizer/ThreadSanitizer 跑原生代码。

展开：Miri 的用法是 cargo +nightly miri test，它把程序当 MIR 解释执行，为每次内存访问维护指针溯源（provenance）和借用栈（Stacked Borrows / Tree Borrows 模型），越界、use-after-free、通过非法别名写内存都会报错并给出详细回溯。代价是慢几个数量级，且不支持所有外部函数调用（FFI 重的代码覆盖有限）。Loom 专攻并发：在穷举的线程交错下跑同一段并发代码，验证无锁数据结构在所有合法调度下的正确性。易错点：Miri 通过不代表代码安全——它只证明已执行路径无 UB，测试覆盖率仍是前提；反过来 Miri 报错基本都是真问题。

cargo +nightly miri test            # UB 检测
cargo test --features loom          # loom 模型化并发测试
RUSTFLAGS="-Z sanitizer=address" cargo test -Z build-std  # ASan

追问方向：Stacked Borrows 模型的核心思想、安全抽象边界的 review 清单（每个 unsafe 块配 safety 注释）。