foundations-formal-methods

用途

形式化方法基础（Formal Methods Foundations）用于证明协议与代理工作流的正确性。其宗旨是把一项需求转化为可检查的性质，选择能捕获该类缺陷的最廉价方法，并精确报告证据究竟确立了什么。资料明确指出：经过验证的有限抽象，只是关于该抽象的证据；实现层面的正确性需要另行证明模型与实现之间的对应关系。

何时使用

触发场景包括：证明某协议正确、编写 TLA+ / PlusCal 规格、对工作流做模型检查、形式化地发现竞态条件、用 Z3 / cvc5 / Lean / Dafny / Verus 做验证、在 TLA+ 与基于性质的测试之间做选择、检查 LLM 生成的证明或规格、判断是否存在某种策略组合允许 X、安全性与活性、细化映射、寻找反例。

以下情况不适用本技能：常规单元测试或 PBT 测试框架属于 qa-testing-strategy；共识、复制与租约设计、确定性模拟以及 Jepsen 历史记录属于 foundations-distributed-systems；代理行动的危害分析属于 foundations-safety-engineering。当规格本身、验证方法的选择或结果的含义是核心问题时，才使用本技能。

方法阶梯

资料给出了按缺陷类别选择最廉价恰当方法的原则：

边界情况输入、顺序逻辑：使用基于性质的测试或模糊测试，结果表示在采样输入中是否发现缺陷。
真实代码中的罕见交错：使用确定性模拟，结果表示在探索的种子中是否发现缺陷。
设计竞态、重试、失败、交接：使用 TLA+/PlusCal（TLC）、P、Alloy 6，符号检查可用 Apalache；完成的穷尽检查覆盖有限模型，P 的调度测试和有界符号检查只覆盖其报告过的探索范围。
策略或配置等价性、某输入能否到达 X：使用 SMT（Z3、cvc5）；sat 给出见证，unsat 对其编码成立，unknown 不能证明任何东西。
小规模高价值核心、不限规模：使用 Dafny、Verus、Lean 4、Rocq、Isabelle；针对所述规格与可信基础给出证明。

只有当设计涉及大量交错、授权逻辑、不可逆副作用或激进优化时，才应越过基于性质的测试继续向上攀升。成本、何时不应攀升以及工业证据需阅读 tool-selection.md。

工作流程

陈述需求。指明需求名称、禁止或必需的行为、环境以及观察到的接口。将其归类为状态安全、时序安全、活性或性能需求。参见 specification.md。
构建模型。定义初始状态、变量、迁移、原子性以及环境假设，包括性质所依赖的失败与并发。选择足以表达该类缺陷的常量规模：两个并发行为体是竞态的最小值。记录每一处抽象和每一处被省略的行为。
选择阶梯层级。使用 tool-selection.md 和 model-checking.md，在解释任何结果前先说明范围与工具限制。
运行检查。保留模型、配置、工具版本、性质、结果与轨迹。对每个反例进行分类：系统缺陷、抽象产物，还是错误性质。增加非空洞性探针：良好路径必须可达。
门禁 LLM 输出。若模型起草或编辑了规格、不变式、证明或配置，在接受任何结果前先运行 llm-generated-specs.md 中的门禁。
将结论与代码挂钩。对于关于已部署代码的结论，阅读 refinement.md 并列出对应义务。轨迹一致性是实践中的桥梁。
报告。产出一份 verification-report。使用“在该有限模型中成立”“发现反例”或“不确定”这样的表述。绝不可将有限或有界的结果升级为一般正确性。

代理形态的示例

agent-workflows.md 包含一份经过 TLC 检查的幂等工具调用加重试的规格，展示三点：一是只有两个工作线程时 TLC 才能发现的检查后行动竞态，单工作线程模型会给出错误的“成立”结论；二是第一处修复引入的幻影确认缺陷；三是同时通过两个不变式的协议及其非空洞性探针。同一参考资料还覆盖绑定到参数哈希的审批门、取消、租约以及策略即 SMT。

轻量有限检查器

scripts/check_finite_model.py 在显式、完全枚举的有限图上检查状态不变式，并返回最短违规轨迹。它不检查活性，也不检查代码对应关系。其契约与测试见 finite-checker.md。运行方式为：python3 scripts/check_finite_model.py model.json。

假设与陷阱

不变式必须在初始状态以及迁移之后都成立。不可达的禁止状态不构成对可达状态安全的违反。停顿、行动粒度、调度与公平性会改变时序结论。安全性成功不能确立最终完成。有界的 SAT/SMT unsat 结果只在其编码与界内排除了反例；unknown、超时和部分搜索不构成任何缺失性结论。可满足公式是其编码约束的见证，并不自动是执行；需检查编码并解码见证。对称归约、约束、抽象与被省略的失败，都需要针对每条性质给出理由。过小的常量会隐藏竞态。错误规格的证明不能确立预期需求；需要分别检查需求与实现映射。在将工具语义与版本视为当前有效前，应核对工具当前的第一手文档。引用基准数据时要带上模型、版本与日期。不得把生成的结论、解析器成功或有界搜索呈现为超出其所述证据的证明。

完成标准

有用的结果需指明：性质与模型；假设以及方法与工具及其版本；界与常量；证据及反例状态；非空洞性探针；一致性缺口。直接报告验证失败，绝不可为了让检查通过而悄悄削弱性质。

工具选择：方法阶梯、成本与收益、何时不应使用形式化方法以及工业证据。LLM 生成的规格与证明：验收门禁、逃生舱扫描、非空洞性与变异检查以及基准。代理工作流：经 TLC 检查的幂等重试示例与代理协议性质。规格：需求、不变式、时序性质与非空洞性。模型检查与 SAT/SMT：方法选择、有界结果与反例。细化：将模型映射到需求与实现。有限检查器契约：严格的 JSON schema 与确定性输出。验证报告：输出工作表。来源：每件工具、基准与工业主张背后的第一手材料。

技能介绍

用途