AgentSkillsCN

formal-methods

形式化方法与建模工具。适用于 formal methods、TLA+、Alloy、模型检查、形式化验证等场景。提供 TLA+ 与 Alloy 的建模、验证及实例生成能力。

SKILL.md
--- frontmatter
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.

  1. •

    Send voice notification:

    bash
    curl -s -X POST http://localhost:8888/notify \
  -H "Content-Type: application/json" \
  -d '{"message": "Running formal methods verification"}' \
  > /dev/null 2>&1 &
  2. •

    Output text notification:

    code
    🔬 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.mdTLA+
并发系统建模Workflows/TLA-Concurrency.mdTLA+
关系约束验证Workflows/Alloy-Relations.mdAlloy
实例生成Workflows/Alloy-Instance.mdAlloy
快速建模Workflows/QuickModel.mdTLA+ / Alloy
属性验证Workflows/PropertyCheck.mdTLA+

TLA+ 适用场景

  • •协议正确性（ Paxos、Raft、2PC）
  • •状态机转换
  • •并发算法
  • •业务流程验证

Alloy 适用场景

  • •结构建模（实体关系）
  • •约束验证
  • •实例生成
  • •反例发现

TLA+ 工作流

核心语法速查

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
==================================================================

标准模板

tla
------------------------- 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 工作流

核心语法速查

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

标准模板

alloy
-- 模块: [名称]
-- 验证目标: [约束]

-- 基础签名
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 工作流

用于验证协议状态机

code
步骤1: 理解协议
    └── 状态有哪些？转换规则？不变量？

步骤2: 编写TLA+ Spec
    └── 常量定义、变量声明、不变式、动作

步骤3: Model Check
    └── TLC运行，检查不变式违反

步骤4: 修复
    └── 迭代直到无错误

Alloy-Relations 工作流

用于关系约束建模

code
步骤1: 识别实体
    └── 有哪些对象？关系是什么？

步骤2: 定义签名
    └── 编写sig声明

步骤3: 添加约束
    └── 编写fact约束

步骤4: 验证
    └── check/srun命令

输出格式

TLA+ 验证报告

markdown
# TLA+ 验证报告: [模块名称]

## 1. 验证目标
- 不变式: [名称]
- 活性: [名称]

## 2. 模型参数
- 状态数量: N
- 深度限制: M

## 3. 验证结果
| 检查项 | 结果 | 说明 |
|--------|------|------|
| TypeOK | ✅ 通过 | 类型正确 |
| Invariance | ✅ 通过 | 不变式满足 |
| Liveness | ⚠️ 需要手动 | 活性验证 |

## 4. 发现的问题
[如有]

## 5. Spec 代码
\`\`\`tla
[代码]
\`\`\`

Alloy 验证报告

markdown
# Alloy 验证报告: [模型名称]

## 1. 验证目标
- 属性: [名称]
- 作用域: N

## 2. 验证结果
| 检查项 | 结果 | 反例 |
|--------|------|------|
| property | ✅ 无反例 | - |
| constraint | ⚠️ 有反例 | 见下文 |

## 3. 实例示例
\`\`\`alloy
[生成的实例]
\`\`\`

集成模式

与architecture-design协作

markdown
## 形式化验证流程

1. **架构设计**
   → architecture-design skill 完成C4建模

2. **关键逻辑识别**
   → 识别需要形式验证的核心逻辑
   → Protocol状态机、角色交互规则

3. **形式化建模**
   → 本skill完成TLA+/Alloy建模

4. **验证**
   → Model Check
   → 修复问题

5. **文档化**
   → 写入架构文档

使用示例

示例1: 验证Protocol状态机

  1. •识别Protocol: R → A → C → D
  2. •编写TLA+:
    • •状态: {idle, R, A, C, D}
    • •转换: 符合协议规则
    • •不变式: 不会死锁
  3. •TLC验证
  4. •生成报告

示例2: 验证角色交互约束

  1. •识别实体: Builder, Devil, Sage, Keeper
  2. •编写Alloy:
    • •sig Role {}
    • •fact: 每个阶段必须有角色参与
  3. •实例生成
  4. •验证约束

质量标准

  • •每个TLA+ spec必须有TypeOK和关键不变量
  • •每个Alloy model必须有事实约束
  • •验证结果必须记录在文档中
  • •反例必须分析并修复

资源

工具: TLA+, Alloy, TLC, Alloy Analyzer