解读

Prusti 是 Rust 社区中唯一成熟开源的静态验证器，它基于 Viper 中间语言，在编译期对函数的前置条件、后置条件、循环不变式进行形式化证明。国内头部互联网与金融科技公司在面试“安全底层系统”或“高可信组件”岗位时，常把“能否用 Prusti 给关键路径加证明”作为区分普通开发与系统级人才的试金石。面试官真正想听的不是“跑通 hello_prusti”，而是：

1. 你能否在真实业务代码里按需添加规范而不拖垮编译速度；
2. 遇到路径爆炸或循环无法终止时，如何拆解证明义务；
3. 在CI 流水线里如何卡点——证明不过，版本打不了 tag；
4. 与unsafe 边界、FFI、async 共存时的最小化隔离策略。

知识点

• Prusti 架构：Rustc → Prusti 驱动 → Viper 中间语言 → Silicon / Carbon 后端 SMT 求解器
• 规范语言：#[requires(...)]、#[ensures(...)]、#[pure]、#[trusted]、body_invariant!
• 证明义务生成：路径敏感、模块化、按需惰性实例化
• 常见无法自动证明的模式：非线性算术、位运算、递归归纳、动态 borrow
• 性能调优：prusti-contracts feature 开关、量化器触发器、SMT 超时参数、#![prusti::check_overflow(false)]
• CI 集成：Docker 镜像 prusti-dev/prusti-ci，GitHub Action cargo-prusti，失败阈值 PRUSTI_FAIL_ON_WARN=true
• 与 unsafe 的边界：#[trusted] 只能放在最小化封装层，并手写对应规范；禁止对业务逻辑直接使用
• 异步支持现状：截至 2024 Q2，async-fn 仍无法被 Prusti 直接验证，需拆成同步状态机或用 stub 规范

答案

“我在生产环境落地 Prusti 分四步，每一步都可回滚：

1. 环境锁定
   用 rust-toolchain.toml 把 nightly 日期锁在 Prusti 官方支持的版本，例如 nightly-2024-05-15；CI 镜像基于 prusti-dev/prusti-ci:0.3.2，防止 Rustc 升级导致证明突然失效。

2. 模块级试点
   先选无 unsafe、无 async 的纯算法模块，例如内存分配器的空闲链表。给核心函数加 #[pure] 与 #[requires(slice.len() > 0)]，跑 cargo prusti --release --verbose，把第一次爆出的 37 条警告全部写成 body_invariant! 或辅助引理函数，保证 0 warning 后才合并到 main。

3. unsafe 边界隔离
   对位图里需要 unsafe { std::ptr::write_bytes } 的清零路径，我封装成 #[trusted] unsafe fn clear_page(ptr: *mut u8)，并在规范里显式写出后置条件：ensures(forall(|i: usize| (0 <= i && i < 4096) ==> ptr.wrapping_add(i).read() == 0))。整个 crate 里只有这 12 行 unsafe，其余 4000+ 行全部被 Prusti 证明，审计时只 review trusted 块。

4. CI 卡点与性能兜底
   在 GitLab CI 里加 cargo prusti --timings=json | jq '.total_time' 若大于 120 秒则自动降级为 nightly 定时任务，但阻塞 release 分支；同时把 PRUSTI_SMT_QI_EAGER_THRESHOLD=1000 调低，防止量化器爆炸。上线三个月，编译增量时间平均增加 8.7%，但内存安全缺陷从 2 个/月降到 0。”

拓展思考

• 当 Prusti 无法证明递归红黑树时，你会如何手动写归纳引理？是否考虑用 #[extern_spec] 把标准库 Vec 的 push 规范前置导入，从而复用已有证明？
• 在嵌入式 no_std 环境，LLVM 后端被换成 riscv32imc，Prusti 无法直接调用 Silicon 后端，你是否愿意把 Viper IR 导出到宿主机做交叉证明？
• 如果公司代码需通过 GB/T 34943-2017 安全认证，审计员要求每一条 trusted 函数必须配套 Coq 手写证明，你能否把 Prusti 规范自动转译到 Coq？这在国内金融 IC 卡芯片领域已是显性需求。