劳动的 LCF

vibe-linter 真正所属的范畴。它的节点不是行为已指定的过程（workflow 说的是"发生了什么"）；它们内部是随机的——这张图只描述什么算作完成，以及各条"完成证明"之间的依赖顺序。步骤是存在量化的："∃ 一次执行，使 validator 通过"。所以这张网是一个证明义务的结构。

五十年前的先例是LCF 架构（HOL、Isabelle）：证明的搜索过程不可信（任何 tactic 都行，哪怕是神经网络生成的），但 thm 是一个抽象数据类型，其唯一的构造子就是可信内核的推理规则。对应关系：

agent = tactic · validator = kernel 推理规则 · token = thm

节点的语义 = 一个 Hoare 三元组 {hold these tokens} stochastic-blackbox {validator passes}，其中 fuel/timeout/escalation 构成失败的本体论语义（完成只是一种希望）。"离它最近的亲戚不是 Airflow，而是 Isabelle——一位逻辑学家兜了一个大圈子，又回来造了一个证明助手，只不过这一次 tactic 要花钱。"

这也是为什么它是一个识别器（recognizer），而不是生成器 → recognizer-not-generator。

上级：vibe-linter