| name | formal-methods |
| description | 形式化方法与建模工具。USE WHEN formal methods, TLA+, Alloy, model checking, formal verification, 形式化, 形式验证, 状态机建模, 模型检查, 协议验证, property verification. 提供TLA+和Alloy的建模、验证、实例生成能力。 |
| implements | Science |
| science_cycle_time | macro |
| context | fork |
Customization
Before executing, check for user customizations at:
~/.claude/skills/PAI/USER/SKILLCUSTOMIZATIONS/formal-methods/
If this directory exists, load and apply any PREFERENCES.md, configurations, or resources found there. These override default behavior. If the directory does not exist, proceed with skill defaults.
🚨 MANDATORY: Voice Notification (REQUIRED BEFORE ANY ACTION)
You MUST send this notification BEFORE doing anything else when this skill is invoked.
-
Send voice notification:
curl -s -X POST http://localhost:8888/notify \
-H "Content-Type: application/json" \
-d '{"message": "Running formal methods verification"}' \
> /dev/null 2>&1 &
-
Output text notification:
🔬 Running the **formal-methods** skill for [purpose]...
This is not optional. Execute this curl command immediately upon skill invocation.
formal-methods Skill
形式化方法与建模工具，用于复杂系统的精确建模与验证。
核心概念
什么是形式化方法？
形式化方法是使用数学精确语言来描述、验证和分析软件/硬件系统的方法。
| 方法 | 工具 | 擅长 |
|---|
| 状态机建模 | TLA+ | 并发、协议、流程 |
| 关系模型 | Alloy | 结构约束、实例生成 |
| 定理证明 | Coq | 数学证明、编译器验证 |
| 模型检查 | SPIN | 并发验证 |
何时使用形式化方法？
- 关键系统（生命安全、金融）
- 复杂并发逻辑
- 协议设计（分布式共识）
- 状态机转换规则
- 约束条件验证
Workflow Routing
Route to the appropriate workflow based on the request.
工具选择
| 场景 | 工作流 | 工具 |
|---|
| 协议状态机验证 | Workflows/TLA-Protocol.md | TLA+ |
| 并发系统建模 | Workflows/TLA-Concurrency.md | TLA+ |
| 关系约束验证 | Workflows/Alloy-Relations.md | Alloy |
| 实例生成 | Workflows/Alloy-Instance.md | Alloy |
| 快速建模 | Workflows/QuickModel.md | TLA+ / Alloy |
| 属性验证 | Workflows/PropertyCheck.md | TLA+ |
TLA+ 适用场景
- 协议正确性（ Paxos、Raft、2PC）
- 状态机转换
- 并发算法
- 业务流程验证
Alloy 适用场景
- 结构建模（实体关系）
- 约束验证
- 实例生成
- 反例发现
TLA+ 工作流
核心语法速查
------------------------- MODULE ModuleName -------------------------
EXTENDS Naturals, Sequences, FiniteSets
\* 常量
CONSTANTS
\* @type: Int;
MaxValue
\* 变量
VARIABLES
\* @type: Str;
state,
\* @type: Set(Str);
history
\* 类型断言
TypeOK ==
state \in DOMAIN history
\* 不变式
Invariance ==
LET Sum == ... IN
Sum <= MaxValue
\* 动作
Next ==
\/ /\ state = "idle"
/\ state' = "running"
\/ /\ state = "running"
/\ state' \in {"success", "failure"}
\* 定理
THEOREM Spec => []Invariance
==================================================================
标准模板
------------------------- MODULE protocol -------------------------
\* 协议名称: [名称]
\* 验证目标: [不变式/活性]
EXTENDS Naturals, Sequences
VARIABLE
\* @type: Str;
pc,
\* @type: Set(Str);
msgs
\* 初始化
Init ==
pc = "start" /\ msgs = {}
\* 动作
Next ==
\/ SendMessage
\/ ReceiveMessage
\/ Terminate
\* 完整规格
Spec == Init /\ [][Next]_vars
\* 不变式
TypeOK ==
pc \in {"start", "sending", "receiving", "done"}
\* 活性
Liveness ==
pc = "start" ~> pc = "done"
==================================================================
Alloy 工作流
核心语法速查
-- 签名定义
sig Entity {
field: some Type,
relation: lone RelatedEntity
}
-- 事实约束
fact {
-- 约束1
all x: Entity | x.field != none
-- 约束2
no x: Entity | x in x.^relation
}
-- 断言
assert Invariant {
all x: Entity | condition[x]
}
-- 检查命令
check Invariant for 5
标准模板
-- 模块: [名称]
-- 验证目标: [约束]
-- 基础签名
sig Node {
outgoing: set Node,
label: one Label
}
sig Label {}
-- 事实约束
fact {
-- 无环
no iden & ^outgoing
-- 连通性
all n: Node | Node in n.*outgoing
}
-- 验证属性
pred property_holds {
-- 属性描述
}
check property_holds for 3
-- 实例生成
run example for 5
Workflows 详情
TLA-Protocol 工作流
用于验证协议状态机
步骤1: 理解协议
└── 状态有哪些？转换规则？不变量？
步骤2: 编写TLA+ Spec
└── 常量定义、变量声明、不变式、动作
步骤3: Model Check
└── TLC运行，检查不变式违反
步骤4: 修复
└── 迭代直到无错误
Alloy-Relations 工作流
用于关系约束建模
步骤1: 识别实体
└── 有哪些对象？关系是什么？
步骤2: 定义签名
└── 编写sig声明
步骤3: 添加约束
└── 编写fact约束
步骤4: 验证
└── check/srun命令
输出格式
TLA+ 验证报告
# TLA+ 验证报告: [模块名称]
## 1. 验证目标
- 不变式: [名称]
- 活性: [名称]
## 2. 模型参数
- 状态数量: N
- 深度限制: M
## 3. 验证结果
| 检查项 | 结果 | 说明 |
|--------|------|------|
| TypeOK | ✅ 通过 | 类型正确 |
| Invariance | ✅ 通过 | 不变式满足 |
| Liveness | ⚠️ 需要手动 | 活性验证 |
## 4. 发现的问题
[如有]
## 5. Spec 代码
\`\`\`tla
[代码]
\`\`\`
Alloy 验证报告
# Alloy 验证报告: [模型名称]
## 1. 验证目标
- 属性: [名称]
- 作用域: N
## 2. 验证结果
| 检查项 | 结果 | 反例 |
|--------|------|------|
| property | ✅ 无反例 | - |
| constraint | ⚠️ 有反例 | 见下文 |
## 3. 实例示例
\`\`\`alloy
[生成的实例]
\`\`\`
集成模式
与architecture-design协作
## 形式化验证流程
1. **架构设计**
→ architecture-design skill 完成C4建模
2. **关键逻辑识别**
→ 识别需要形式验证的核心逻辑
→ Protocol状态机、角色交互规则
3. **形式化建模**
→ 本skill完成TLA+/Alloy建模
4. **验证**
→ Model Check
→ 修复问题
5. **文档化**
→ 写入架构文档
使用示例
示例1: 验证Protocol状态机
- 识别Protocol: R → A → C → D
- 编写TLA+:
- 状态: {idle, R, A, C, D}
- 转换: 符合协议规则
- 不变式: 不会死锁
- TLC验证
- 生成报告
示例2: 验证角色交互约束
- 识别实体: Builder, Devil, Sage, Keeper
- 编写Alloy:
- sig Role {}
- fact: 每个阶段必须有角色参与
- 实例生成
- 验证约束
质量标准
- 每个TLA+ spec必须有TypeOK和关键不变量
- 每个Alloy model必须有事实约束
- 验证结果必须记录在文档中
- 反例必须分析并修复
资源
工具: TLA+, Alloy, TLC, Alloy Analyzer
