该技能是一份形式化验证实践指南，重点不在于某个具体工具的操作手册，而在于两件事：如何为问题挑选最轻量的合适方法，以及如何判断一次验证结果到底确立了什么。
用途与选型。技能主张默认先采用基于性质的测试、模糊测试、故障注入或确定性模拟；只有当输入或交错空间大到无法采样、且漏掉一个用例代价高昂时，才转向形式化方法。给出的对应关系是：并发或分布式协议设计做模型检验，默认用 TLA+；输入空间巨大的小型对抗性单元做有界模型检验，Rust 用 Kani，C 用 CBMC；解析器、加密、授权、分配器等以正确性为产品的代码使用自动主动验证器，如 Dafny、Verus、SPARK；数学命题或已验证的系统模型使用 Lean 4。若缺陷已进入生产，能复现它的故障注入通常优于建模；在选择修复方案时则应对设计建模，因为在一个执行轨迹中有效的修复在另一条轨迹中仍可能失败。
陈述即产品。技能要求先用平实语言写出性质，再形式化；不变式、定理、契约须由人签核后才能开始证明。代理可以提出性质，但不能决定“正确”的含义。已批准的陈述要冻结：证明过程中只能添加证明提示、引理和循环不变式，绝不能修改陈述、弱化前置条件或强化假设；陈述变更须带差异回到签核环节。还要求最偷懒的错误实现必须无法通过规格，例如返回空列表的排序在“已排序”上成立，因此规格还需包含“是原列表的排列”；模型不得假设自己的答案，例如把支付提供商建模为完美的去重器，就无法证明修复的有效性，此类假设必须在报告中列为假设；原子性要与真实系统一致，每个真实原子步骤（一条 SQL、一次 RPC、一次系统调用）对应一个动作，把读写捆绑在一个动作里会掩盖要找的竞争。
通过必须见过失败。技能要求埋入缺陷并观察其被抓到：破坏算法（去掉锁、交换两个步骤、移除修复）并确认性质以合理的反例失败；能幸存自身缺陷的性质是空洞的。还要证明关键状态可达，使用应当失败的金丝雀性质（如 ~(all jobs done)、kani::cover!）以及覆盖信息确认每个动作都被触发。不得静默关闭检查：TLC 的 -deadlock 会禁用死锁检查，{:verify false}、--no-verify 和宽松的展开界限同理；若确需使用，须说明是哪一个及原因，并补上它原本替代的性质（终止性、进展性）。安全性只是一半，至少要检查一条活性性质（如“每个被认领的任务最终完成”），显式陈述公平性，并确认本应失败的活性性质确实失败。
审计与报告。构建工具会在证明未完成时报告成功，如 lake build 带 sorry 仍以 0 退出、Lean 公理不打印警告、Bend 在导入文件中的 @unsafe 干净通过；代理可测量地利用这些逃逸口完成证明。因此宣称已验证前要运行工具自带审计并搜索逃逸口，残留的逃逸口须作为假设报告，不得隐藏。每份结果都应说明：声明（性质的自然语言表述及被检查的产物，如文件、定理或性质名）；强度（无界证明、在所列界限内有模型检验、或未检查的草稿）；假设与可信基（公平性、环境抽象、残留逃逸口、工具所信任的编译器、FFI、SMT 求解器等）；与代码的链接（是否有轨迹验证、生成测试、对已验证模型的差分测试，或明确仅限设计）；以及是否见过失败（埋入的缺陷或金丝雀）。
工具链与限制。工具应安装到项目或临时目录而非系统全局，锁定精确的稳定版本而非滚动预发布版或 latest，并在项目发布校验和时验证校验和；报告中记录版本，因为检查器缺陷按发布逐个修复。技能还附带参考文档入口，分别覆盖方法选择与成本证据、逃逸口与审计命令、TLA+、PlusCal、Quint 与 TLC 配置及活性与轨迹验证、Lean 4 的设置与证明循环及验收门槛、Bend 2 的定律与证明；evals 目录存放该技能的测试提示与断言。限制在于工具知识过时很快，描述某个工具前应查阅实时文档。资料未提供具体安装命令、代码示例或定价信息，需另行查阅官方文档。