Formal Model Checking 是一个面向有状态协议的形式化模型检查技能，用于针对并发、重试、持久化与恢复等场景中的有限状态规格，核查一条精确的设计断言。其目标是用小型、可执行的状态模型验证设计层面的性质，而不是替代实现测试或等价性证明。
主要能力与工作流程：
-
界定断言范围。明确待验证性质、初始状态、参与者/取值边界、假设条件与授权交付物，并区分安全性（safety）与活性（liveness）；记录输入版本、检查器版本与配置。
-
保留真实边界。将待提交（pending）与已提交（committed）状态分开；在相关时纳入竞争参与者与失败/恢复步骤；注意崩溃不会执行 catch 或 finally，异常不能作为替代；若断言覆盖所有操作则需保留历史；对任何原子模型步骤给出理由。
-
执行并解读结果。真实反例是有价值的，可用于完成缺陷发现或设计任务；对于正面结论，要求完整搜索、一个违反预期不变式的不安全变体及其轨迹，以及可达的成功路径和重要失败路径。解析错误、超时、错误的不变式或不可达的成功都不构成该证据。
-
与代码衔接（当代码存在时）。将模型动作映射到具体边界并记录未验证义务；若要验证或修复实现，需针对实际状态与效果复现反例，建立失败基线并验证修正；进程丢失断言需要独立 worker、已确认的检查点与已验证的终止；模拟的边界调用不能证明运行时行为。
-
诚实报告。将模型结果、实现测试、边界、假设、排除项与未完成检查分开陈述；测试不提供形式化精化或等价性证明；有限穷举图只覆盖被建模的执行长度，深度受限搜索只覆盖已探索的长度。
适用场景：有状态协议、并发控制、重试逻辑、持久化与恢复的设计核查，以及需要 TLA+/TLC 形式化检查的请求。
限制与边界：仅做设计工作时，运行时一致性明确保持未验证，且不修改应用行为或 CI；在维护实现的职责内，保留模型到代码的映射与可重复运行的检查；不强行引入全局锁、协调器、outbox 或未要求的部署架构；常规测试和调试不会仅因该技能存在而自动获得模型检查要求。技能附带评估用的评分标准、选择查询与自包含 fixture，但这些不是运行时必需工具，也不构成技能有效性的实测证明。