用途
formal-verify 用于对代码中的并发协议、顺序不变量与 Rust 函数做形式化检查，并把验证结果对应回源码。它覆盖三类目标：线程交错导致的协议缺陷、依赖算术或顺序转移的性质、Rust 函数在边界输入下的行为。
工具选择
- TLA+ 配合 TLC：检查线程交错问题，例如丢失唤醒、资源被释放两次、条目重复或乱序投递、关闭被阻塞、错误在错误线程上报。TLC 会探索小规模实例的状态并给出反例。
- Kani：检查循环有界的 Rust 函数中的溢出、越界访问、panic 与不变量破坏。它直接检查真实代码在给定边界内的每个输入。
- Lean 4：处理算术或顺序转移，例如越界、不变量或编码器往返失败，或到达代码假定不可达的状态。可先评估有界实例，再对任意规模证明性质。
当函数是 Rust 且输入与循环可界定时，优先用 Kani；当性质必须对所有规模成立，或代码不是 Rust 时，用 Lean。若线程协议依赖算术（如 slot = item mod window），需要两者配合：TLA+ 把算术视为常量检查交错，Lean 检查算术本身。用户指定了工具时使用指定工具，并说明它未覆盖的部分。
使用方式
- 选取目标：在源码中搜索线程与协议相关符号和状态名，区分手写协议、数据并行循环、库自带通道或执行器。为每个目标记录线程、共享变量、等待与唤醒、终止状态、所有权转移的资源等；Rust 目标另记输入范围、循环边界与假设。
- 准备工具：通过技能自带的脚本安装或校验 TLC、Lean、Kani 环境；成功时返回 READY，无法运行时返回 UNAVAILABLE 并退出码 3，应报告为“未检查”。
- 每个目标由一个代理建模，代理只写自己的文件，互不共享。
- 把反例读回代码：将轨迹中各步骤映射到代码事件与行号，结合真实常量与调用方判断可达性；可达的反例用确定性测试、竞态检测或压力循环复现。
- 保留证明并统一记录结果：模型头部注释、变异文件、测试文档与 PR 描述各承担一项记录职责，不重复粘贴运行表或轨迹。
适用场景
适合手写线程协议（交接、有界流水线、有序输出队列、关闭清理、重试与租约循环）、依赖算术的协议性质、可界定输入范围的 Rust 函数，以及需要在提交或 PR 中附带形式化证据的修复流程。
限制
这些模型不检查互斥锁以下的内存序，仍需保留项目原有的 ThreadSanitizer 或竞态检测；浮点结果按取整后的整数建模，除非性质本身涉及取整。TLA+ 或 Lean 通过只在其声明的假设下成立，且模型是手工对应代码；Kani 只覆盖报告中的输入与展开边界。任何结果都不代表整个程序正确。未提供具体版本要求、收费标准或平台支持范围。