formal-verify

formal-verify

当架构意图比“代码能编译”更重要时，请使用此技能。

此技能会运行一个三层验证循环：

1. 第 1 层：根据提取的 AST 事实和声明式规则进行结构验证
2. 第 2 层：根据 Z3Py 协议规范和 TLA+/Apalache 状态机规范进行行为验证
3. 第 3 层：根据复杂度、一致性和工艺启发式进行优雅度审查

各层按预定层级运行：

• 每次编辑：仅运行第 1 层，速度足以支持持续反馈
• 切片检查点：运行第 1 层和第 2 层
• 提交前和手动执行 /verify：运行全部三层

快速开始

使用以下命令为目标项目进行引导：

/verify --bootstrap

引导过程分为四个阶段：

1. 安装依赖项并创建 .verifier/
2. 根据文档和代码结构发现架构规则
3. 用通俗英语询问用户存在歧义的地方
4. 根据当前代码库验证初始规则

命令

• /verify 以详细模式运行所有层并打印统一报告。
• /verify --bootstrap 安装依赖项，创建 .verifier/，并搭建第一组规则。
• /verify --evolve 检查架构文档与现有验证规范之间是否存在偏差。
• /verify --grade 仅运行第 3 层，并报告当前优雅度等级。

验证流程

第 1 层：结构验证

运行器会从 Rust 和 Swift 源文件中提取事实，然后检查 structural.yaml 中的规则，例如：

• 只有模块 X 可以跨越边界 Y
• 匹配模式 Z 的模块必须实现接口 W
• 所有模块都不得引用旧版标识符

结构检查是默认的 PostToolUse hook，因为它们速度最快。

第 2 层：行为验证

行为验证涵盖状态转换和协议约定：

• 使用 TLA+/Apalache 验证时序属性、活性和交错执行
• 使用 Z3Py 规范文件验证约定、不变量和跨边界数据保证

在切片检查点、风险较高的合并前，以及任何涉及协调逻辑或跨语言约定的更改中使用此层。

第 3 层：优雅度审查

优雅度审查会从以下方面为代码评分：

• 复杂度
• 一致性
• 工艺

它会给出等级和逐行扣分，让 Agent 能够清理代码， 而不只是确保代码在技术上正确。

违规处理

发现违规时，应根据受众调整输出内容：

• Agent 输出：反例、诊断和具体的修复建议
• 人类输出：仅提供反例和诊断

如果 Agent 连续三次未能解决同一违规，应停止修复循环 并升级问题，同时提供：

• 原始规则
• 反例
• 三次尝试的修复方案
• 目前仍可能阻碍正确修复的问题

在目标仓库中创建的项目结构

引导过程会创建并维护：

.verifier/
├── structural.yaml
├── elegance.yaml
├── specs/
├── facts/
└── reports/

• structural.yaml 存储声明式第 1 层规则
• elegance.yaml 存储阈值和等级策略
• specs/ 存储 Z3Py 和 TLA+ 行为规范
• facts/ 缓存提取的 AST 事实
• reports/ 存储最近的验证输出

目标项目应将 facts/ 和 reports/ 添加到 gitignore。

操作指南

• 在宣称迁移已完成前运行 /verify。
• 如果代码正确但仍显粗糙，请运行 /verify --grade。
• 架构有意演进时，优先更新规则和规范，而不是放宽规则和规范。
• 让 SKILL.md 专注于编排；详细机制请参阅下方的参考资料。

参考资料

• @references/layer1-structural.md 事实提取、Z3 编码、可达性和增量失效处理。
• @references/layer2-behavioral.md 何时使用 TLA+/Apalache 而非 Z3Py，以及规约执行契约。
• @references/layer3-elegance.md 指标类别、评级、阈值和 Layer 3 子模块布局。
• @references/constraint-yaml-spec.md 结构规则架构、选择器、断言和事实模式运算符。
• @references/bootstrap-process.md 安装、发现、访谈、验证引导工作流。
• @references/agent-feedback-loop.md 钩子集成、违规注入、重试和升级策略。
• @references/spec-authoring-guide.md 将通俗英文的架构意图转化为形式化规约。