用途
该技能旨在为项目生成一个本地形式化验证技能，聚焦于代码中错误代价最高且测试难以覆盖的部分。它不直接执行验证，而是引导代理完成目标选择、工具选型、技能编写和验证确认，最终留下一个可供后续代理在修改代码时检查属性的项目内技能。
主要能力
- 从代码库中识别值得形式化验证的目标：代码做出的承诺，一旦破坏会伤害用户且测试很少触及。
- 根据问题选择最低成本的工具：模型检查器（如 TLA+）、证明助手、SMT 验证器等。
- 生成项目本地技能文件（如
.claude/skills/<area>/SKILL.md），包含 frontmatter，命名区域而非verify前缀。 - 确保验证忠于代码、能够失败、发现保持为发现、范围诚实、无需工具即可阅读、重跑成本低，并与代码同步。
- 在交接前通过破坏性临时变更证明技能能捕获问题。
使用方式
- 阅读平台映射（在 Codex 或 GitHub Copilot 上需先阅读）。
- 从代码库回答目标选择问题，仅在无法观察时询问用户。
- 根据问题选择工具，并告知用户选择理由。
- 编写项目本地技能，包含覆盖记录和同步提交点。
- 按照生成的技能执行一次，用临时破坏验证其能捕获问题，然后还原。
- 向用户报告验证内容、工具、边界、发现、运行方式及未覆盖范围。
适用场景
适用于任何语言的项目，尤其是存在关键属性（如内存安全、溢出、数据结构不变量、事件顺序）且测试覆盖不足的代码区域。
限制
- 需要用户能安装和运行所选工具。
- 验证范围受模型或边界限制，通过仅代表模型或边界内成立。
- 若语言无可用验证器，需说明并用生成输入测试真实代码。
- 不改变产品代码，除非用户要求。
- 技能需随代码变更维护，可使用
/maintain-formal-verification-skill更新。