Rust Unsafe 审查先写不变量再缩小裸指针范围Unsafe 不是“这里由我保证正确”的注释它要求作者明确编译器暂时无法验证的条件。审查时先写不变量往往比逐行看指针更有效。四类条件要说清检查指针是否非空、正确对齐且仍指向有效对象别名关系是否符合读写规则长度和容量是否来自同一分配析构是否只发生一次。跨线程时再说明 Send、Sync 的依据和对象生命周期。把 Unsafe 包在小函数里对外提供安全类型。原始地址转换、切片构造和 FFI 各自隔离避免一个块同时承担多种证明责任。注释写“调用者必须满足什么”不要重复代码动作。验证不能替代证明单元测试覆盖边界长度、空输入和错误返回Miri、sanitizer 与 fuzzing 用来寻找反例。但测试没有命中不代表不变量成立。每次修改 Unsafe 周边类型时都要重新审查布局、生命周期和析构路径。