用途：为不安全 Rust 的编写、记录、审查、审计与重新设计提供证明级严谨方法，适用于 unsafe 块与函数、unsafe trait 及其实现、裸指针等。
主要能力：先确立精确命题（覆盖精确源码快照、各受支持编译配置、范围内有效使用），先证明源码级 Rust 健全性，再单独陈述涉及具体编译器后端、二进制、平台或部署的附加前提。要求恢复精确的量化论域，保留控制论域表达式（范围、并集、排除、量词、条件与移动策略）及其来源与审计截止点；对集合关系、归一化、枚举、划分、排除与策略合并都当作证明步骤逐步验证。要求证据承载的证明内核：由工件事实、适用的 Rust/标准库公理或明确可信计算基（TCB）前提、已证引理与显式逻辑推出命题，再交给消费者或裁定。坚持局部、字面地求证：独立于现有安全注释识别控制契约，按字面拆解合取、蕴含、量词、时序子句等。要求跨调用与时间追踪数据流，不局限于词法 unsafe 块。新代码要求把不变式承载表示放入最小叶模块并保持字段私有。执行证明工作流：框定命题、框定完整用例域、清点表面与转换、陈述原子义务与内核、构造推导、闭合与挑战、裁定与报告。写入与审查时要求先读 proof-obligations.md，每个证明紧邻最小内聚 unsafe 操作。审计 API 与配置边界时需读 api-boundaries-and-evolution.md 与 configurations-and-generated-code.md，并采用安全表面清单（公开字段、构造器、安全方法、安全 trait 方法、宏生成 API，以及语言可达的 #[doc(hidden)] 安全项）。评估信任与证据时需读 tcb-and-evidence.md。
限制：不得把本技能、Rustonomicon、Unsafe Code Guidelines、RFC、博客、issue 讨论、实现行为、Miri 或常见实践当作 Rust 公理；权威文档含糊或不足时只报告文档缺口与最小缺失命题，不得用直觉修补；未闭合的证书不得出具 PROVED 等结论，而应记 UNPROVED。官方文本未提供具体安装命令、收费与平台信息。