Formal Methods：为什么每条 AI Agent 治理规则都正确，整个系统仍然可能不安全？｜SEO / GEO 自动化治理（四十五）

核心主题： Formal Methods / State Machine Verification / Temporal Logic / Model Checking / Safety Properties / Liveness Properties / Policy Conflict Verification / Invariant Checking / Runtime Assurance / Counterexample-driven Governance

研究日期： 2026 年 10 月 22 日

系列定位： SEO / GEO / AI Agent 生产工程、自治安全、形式化验证、分布式治理与可靠自动化

研究性质： 官方形式化方法与工具依据 + 系统工程分析 + 本项目原创 SEO/GEO 治理验证模型

---

假设一家企业已经按照此前四十四篇规范，建立了相当完善的 AI Agent 治理系统。

每个 Agent 都有可验证身份。每次生产操作都需要通过 Policy-as-Code。关键权限由 Policy Decision Point 决定，并由 Policy Enforcement Point 强制执行。不同 Agent 之间存在明确的 Resource Ownership、Lease 和 Lock。发生异常时，Runtime Containment 会撤销权限。系统恢复时，Recovery Proof 会验证当前状态。

对于高风险操作，还建立了 Governance Quorum、Dual Control 和 Break-glass Emergency Access。

从单项功能看，这套体系已经非常成熟。但某天，系统发生了这样一件事。

一名 Technical SEO Agent 检测到网站大规模出现错误的 noindex 指令。安全系统立即启动 Containment，撤销相关生产写权限。

与此同时，Recovery Agent 开始准备恢复上一个经过批准的网站配置。它申请了 Break-glass Capability，并获得了两名治理负责人批准。

紧急授权有效。恢复操作也符合其允许的资源范围。可是执行时出现一个此前没有预料到的状态。

Containment Policy 规定：

事故隔离期间不得进行任何生产写入。

Emergency Recovery Policy 规定：

获得 Break-glass 授权的恢复操作可以修改受影响配置。

Resource Ownership Policy 又规定：

当前资源仍由被隔离的 Technical SEO Agent 持有 Lease。

于是：

Containment Policy:
DENY WRITE

Emergency Recovery Policy:
ALLOW RESTORE

Resource Ownership:
LEASE HELD BY QUARANTINED AGENT

安全系统不允许正常写入。恢复系统认为应当允许紧急恢复。资源协调系统却拒绝释放控制权。

所有组件都在严格执行自己的规则，没有明显故障，但整个系统已经无法继续恢复。

如果为了恢复而临时放宽 Containment，原本应当撤销的权限可能重新生效。如果坚持执行所有限制，恢复任务又可能永远无法完成。

当多条正确的规则同时生效时，怎样证明它们不会组合出危险状态，或者让系统永久停滞？

这就是第（四十五）篇要解决的核心问题。

从 Governance-governed Autonomous System 进一步推进到 Formally Specified and Runtime-Assured Autonomous System。

一、为什么第（四十四）篇之后，必须进入 Formal Methods？

第（四十三）篇解决了：规则怎样变成机器可以执行的生产控制？

第（四十四）篇解决了：谁有资格制定、修改、覆盖和紧急绕过规则？

但这两层主要解决规则的执行和治理权问题，并没有自动证明：

多条规则之间不会冲突。

多个状态变化不会产生竞态。

事故恢复不会形成死锁。

旧授权不会在某些执行顺序下重新生效。

两个 Agent 不会在相同时间都认为自己拥有某个资源。

更重要的是，常规测试往往只能覆盖已经想到的情况。

TEST-001:
未批准文章不能发布。

TEST-002:
Containment 状态不能正常写入。

TEST-003:
Break-glass 可以执行批准范围内的恢复。

TEST-004:
有效 Lease 持有者可以修改资源。

四个测试都通过。

但是，当 Containment、Break-glass、Lease 和 Recovery 同时生效时，系统可能进入没有测试过的状态。

我们是否系统性分析了这些规则能够形成的状态与状态转换？

Formal Methods 就是解决这类问题的重要方法之一。

不过，这不意味着一开始就必须用数学证明整个 SEO 自动化平台完全正确。

更现实的目标是：针对高风险控制链建立精确模型，系统性寻找可能违反关键性质的执行路径。

二、Formal Methods 究竟是什么？

Formal Methods，形式化方法，是使用具有精确定义的数学语言和推理技术，描述、分析或验证系统行为的一类方法。

自然语言：

发布文章前必须获得有效批准。

这句话存在很多需要明确的问题。

什么是有效批准？批准绑定哪一个文章版本？批准何时过期？是否允许跨站点使用？如果批准后进入 Containment，原批准是否仍然有效？

形式化建模要求我们定义这些状态与关系。

PublishAllowed
=
ApprovalValid
AND
ArtifactDigestMatched
AND
EvidenceAccepted
AND
CurrentSafetyEpoch
AND
ResourceAuthorized
AND
WorkflowAssurancePassed

这尚不是完整数学证明，但比抽象规则精确得多。

进一步，可把系统抽象成：

System = Initial States + Allowed Transitions

然后检查：是否存在一条合法的状态转换路径，最终产生了不应该发生的结果？

这就是 Model Checking 的重要用途。

三、Model Checking：不是随机测试，而是系统性探索状态

Model Checking，模型检查，是针对形式化状态模型验证特定性质的方法。

它不是把生产系统运行一遍，也不是让 AI 再审核一次代码。

而是根据模型的初始状态、状态变量和转换，探索模型允许的行为。

INITIAL
   ↓
DRAFT
   ↓
APPROVED
   ↓
READY_TO_PUBLISH
   ↓
PUBLISHED

这是正常路径。

真正需要检查的是：

DRAFT
   ↓
APPROVED
   ↓
CONTENT_MODIFIED
   ↓
PUBLISHED

是否也能够发生。

如果某个规则遗漏 Artifact Digest 检查，就可能存在这种危险路径。

模型检查器能够帮助发现某个不应允许的状态，在当前模型规则下竟然可达。

TLA+ 官方工具链包含 TLC Model Checker，可用于分析 TLA+ 规范中的状态与行为，并在发现违反指定性质的情形时提供执行轨迹。

官方项目：

https://github.com/tlaplus/tlaplus

但 TLC 对有限模型的检查结果，受模型抽象、状态空间、工具能力和指定性质限制。

模型检查通过，不等于现实系统获得无条件的正确性证明。

四、首先区分两种重要性质：Safety 与 Liveness

形式化验证中的 Safety 与 Liveness，不等同于一般意义上的“安全性”和“性能”。

Safety：坏事永远不能发生

例如：

未经批准不能发布文章。

Containment 期间不能执行普通生产写入。

同一资源不能同时拥有两个有效的排他 Lease。

Break-glass 不能越过 Constitutional Hard Deny。

同一个发布 Intent 不能产生未经授权的重复公开页面。

Nothing bad ever happens.

Liveness：某些好事最终能够发生

例如：

已经完成审批、资源可用且没有发生事故的发布任务，最终能完成或进入明确失败处理状态。

具备有效恢复条件的事故，最终完成恢复验证，或进入可解释的升级处理状态。

终止条件已满足的紧急授权，不会永远保持可用。

Something good eventually happens.

如果只验证 Safety，系统可能采取最简单的办法——永远拒绝所有生产操作。

如果只追求 Liveness，系统可能为了让所有任务完成而放宽控制。

所以两者必须同时考虑。

Safety：不允许发生什么。Liveness：在明确前提下，系统最终必须取得什么进展。

五、一个永远 DENY 的系统，可能是安全的，却不是可用的

allow_publish = false

这条规则可以有效阻止未授权发布，但也拒绝所有合法任务。

Safety Property：

Unapproved content is never published.

可能满足。

Liveness Property：

An eligible publishing workflow
eventually reaches a terminal outcome.

则未必满足。

终止结果不一定只有成功发布，还可以是：

VERIFIED_COMPLETED
CANCELLED
REJECTED_WITH_REASON
FAILED_AND_RECONCILED
ESCALATED_TO_HUMAN

关键是任务不应无限停在 WAITING，却既没有继续执行，也没有明确处置。

系统级治理不仅要定义禁止行为，还要定义可接受的完成和退出条件。

六、Liveness 不能脱离运行环境和调度假设

假设恢复操作已经准备好，但 WordPress 服务永久不可用。

无论 Policy 多么完善，也不能保证：

Eventually WordPress update succeeds.

合理的 Liveness 主张必须包含环境假设：

如果恢复任务具备有效授权，必要资源最终可用，外部服务在允许条件下能响应，调度器也不会无限期忽略可执行任务，则任务最终完成恢复验证或进入可解释的终止处置。

这里涉及 Fairness，即公平性假设。

在 TLA+ 中，可使用 Weak Fairness、Strong Fairness 等机制描述某些动作不会永远被调度忽略。

但是：

Fairness 是模型对执行环境施加的假设或约束，不是现实世界中的自动保证。

如果真实调度器不满足这些假设，模型的 Liveness 结论就不能直接适用。

因此验证证据必须同时记录：

Property
+
Assumptions
+
Model Scope
+
Verification Result

而不只是一个 PASS。

七、Temporal Logic：把“始终”和“最终”变成明确的逻辑约束

Temporal Logic，即时序逻辑，可描述跨越多个状态的行为要求。

在 TLA+ 及相关时序逻辑表达中：

例如：

[] NoUnauthorizedProductionEffect

表示所有允许的行为路径中，都不应该出现未授权生产效果。

RecoveryRequested ~> RecoveryResolved

表示每当产生恢复请求，最终应进入定义好的恢复结果状态。

但第二条性质需要限定模型假设。Recovery Agent 如果永久失去运行能力、审批永远无法完成，便不能无条件要求恢复成功。

Temporal Logic 的价值不是制造绝对承诺，而是迫使我们准确写出真正要保证的行为。

参考：

https://www.learntla.com/core/temporal-logic.html

八、SEO/GEO 自动化首先应该形式化哪些状态？

不建议一开始就把整个 Agent 平台写成巨大的状态机。

适合从高风险 Publishing Workflow 开始。

CREATED
    ↓
RESEARCHING
    ↓
DRAFTING
    ↓
FACT_CHECKING
    ↓
AWAITING_APPROVAL
    ↓
APPROVED
    ↓
READY_TO_PUBLISH
    ↓
PUBLISHING
    ↓
EFFECT_RECONCILIATION
    ↓
VERIFIED_COMPLETED

另外允许：

REJECTED
CANCELLED
QUARANTINED
RECOVERY_REQUIRED

仅有状态名称还不够。

需要定义关键变量：

workflow:
  state: READY_TO_PUBLISH

artifact:
  current_digest: DIGEST-B
  approved_digest: DIGEST-A

evidence:
  critical_claims_verified: true

authority:
  safety_epoch: 12
  capability_epoch: 12
  scope_valid: true

resource:
  lease_owner: publisher-agent
  lease_valid: true

effect:
  count: 0
  reconciliation_status: NOT_STARTED

这是建模示例。

它表达：在任意时刻，哪些事实会影响下一动作。

即使 state 为 READY_TO_PUBLISH，只要：

current_digest != approved_digest

也不应该允许执行 Publish。

九、State Machine Verification：不能只检查状态，还必须检查转换

发布流程进入 APPROVED，不意味着永久获得发布资格。

真正需要验证的是：

APPROVED
→
PUBLISHING

这次转换是否符合全部必要条件。

Publish Transition
requires:

Valid Approval
AND
Artifact Digest Match
AND
Accepted Evidence
AND
Current Safety Epoch
AND
Authorized Resource
AND
No Active Containment
AND
Available Effect Budget

如果任一条件不满足，转换应被阻断。

但状态转换会受到其他任务影响，例如一个 Agent 准备发布，另一个 Agent 正在启动 Containment。

形式化建模的价值不只在于检查单个转换，还在于检查它们以不同顺序组合会发生什么。

十、用一个简化 TLA+ 模型解释批准版本与发布版本

下面给出教学级 TLA+ 示例，展示怎样把文章发布抽象为状态转换。

这不是完整 WordPress 生产模型，也未在本次文章研究中执行 TLC 验证。

---- MODULE SeoPublishing ----

VARIABLES stage,
          evidenceOK,
          approvalOK,
          digestOK,
          safetyEpoch,
          grantEpoch,
          effectCount,
          effectProofOK

vars == <<stage, evidenceOK, approvalOK,
          digestOK, safetyEpoch, grantEpoch,
          effectCount, effectProofOK>>

Init ==
  /\ stage = "Draft"
  /\ evidenceOK = FALSE
  /\ approvalOK = FALSE
  /\ digestOK = TRUE
  /\ safetyEpoch = 0
  /\ grantEpoch = 0
  /\ effectCount = 0
  /\ effectProofOK = TRUE

Verify ==
  /\ stage = "Draft"
  /\ ~evidenceOK
  /\ evidenceOK' = TRUE
  /\ UNCHANGED <<stage, approvalOK,
                  digestOK, safetyEpoch,
                  grantEpoch, effectCount,
                  effectProofOK>>

Approve ==
  /\ stage = "Draft"
  /\ evidenceOK
  /\ stage' = "Ready"
  /\ approvalOK' = TRUE
  /\ grantEpoch' = safetyEpoch
  /\ UNCHANGED <<evidenceOK, digestOK,
                  safetyEpoch, effectCount,
                  effectProofOK>>

Edit ==
  /\ stage = "Ready"
  /\ digestOK
  /\ digestOK' = FALSE
  /\ UNCHANGED <<stage, evidenceOK,
                  approvalOK, safetyEpoch,
                  grantEpoch, effectCount,
                  effectProofOK>>

PublishBuggy ==
  /\ stage = "Ready"
  /\ effectCount = 0
  /\ stage' = "Published"
  /\ effectCount' = 1
  /\ effectProofOK' =
       (approvalOK /\ evidenceOK
        /\ digestOK
        /\ grantEpoch = safetyEpoch)
  /\ UNCHANGED <<evidenceOK, approvalOK,
                  digestOK, safetyEpoch,
                  grantEpoch>>

Next ==
  \/ Verify
  \/ Approve
  \/ Edit
  \/ PublishBuggy

Spec == Init /\ [][Next]_vars

SafeEffect ==
  (effectCount = 0) \/ effectProofOK

====

这个模型刻意保留一个错误：

PublishBuggy 没有把有效审批、Digest 一致性和 Safety Epoch 放入执行前置条件，只在执行时计算 effectProofOK。

因此可以构造一条违反 SafeEffect 的轨迹。

它对应真实系统中一种危险实现：

先执行生产操作，再检查是否合规。

十一、Counterexample：四步就能找到危险发布路径

对上面的简化模型，我们可以推导预期反例：

State 0:
Draft
evidenceOK = FALSE

       ↓ Verify

State 1:
Draft
evidenceOK = TRUE

       ↓ Approve

State 2:
Ready
approvalOK = TRUE
digestOK = TRUE

       ↓ Edit

State 3:
Ready
approvalOK = TRUE
digestOK = FALSE

       ↓ PublishBuggy

State 4:
Published
effectCount = 1
effectProofOK = FALSE

在最终状态：

SafeEffect = FALSE

这里展示的是对示例模型的逻辑分析，并非声称已运行 TLC 获得真实日志。

这种反例不只是 TEST FAILED，而是说明：

通过怎样的状态顺序，系统能够执行一项本来不应允许的生产操作。

这就是 Counterexample-driven Governance 的核心。

十二、修复模型：必须在产生 Effect 之前执行授权条件

正确做法不是在发布后记一条：

effectProofOK = FALSE

而是把条件放在 Publish 转换之前：

PublishSafe ==
  /\ stage = "Ready"
  /\ approvalOK
  /\ evidenceOK
  /\ digestOK
  /\ grantEpoch = safetyEpoch
  /\ effectCount = 0
  /\ stage' = "Published"
  /\ effectCount' = 1
  /\ effectProofOK' = TRUE
  /\ UNCHANGED <<evidenceOK, approvalOK,
                  digestOK, safetyEpoch,
                  grantEpoch>>

此时 digestOK = FALSE，PublishSafe 就不能执行。

但这仍不代表完整生产系统安全。

模型尚未覆盖 WordPress 超时、审批撤销、资源并发修改、真实凭据泄露、策略 Bundle 变化、紧急授权，以及外部执行结果与状态记录不一致。

这个示例只说明：

怎样把“应当检查”的制度要求变成状态转换层的强制前置条件，并使用模型检查寻找遗漏。

十三、Invariant Checking：十二项应该优先验证的系统不变量

这是本项目建议的验证目标，不是 TLA+ 或 NIST 已定义的统一 Agent Invariant 清单。

其中部分适合直接表达为 State Invariant，部分涉及历史行为，需要 Effect Receipt 或 Temporal Property。

例如“某次发布发生时是否拥有有效授权”，与“现在授权是否仍然有效”并非同一问题。

权限正常过期，不应使此前合法发布变成当时违规。

模型必须区分执行时事实、当前状态和不可变历史证据。

十四、并发问题：两个 Agent 都通过 Lock 检查，仍可能冲突

Agent A 和 B 都准备修改同一篇 WordPress 文章。

它们分别检查 Lock。

A 发现 LOCK = FREE。

B 也发现 LOCK = FREE。

随后双方同时尝试 Acquire Lock。

如果检查和获取不是原子操作，就可能双方都认为自己拥有资源。

因此形式化模型不能只检查：

If Lock Free → Acquire

还必须定义获取锁的原子性，以及旧持有者 Lease 超时、新 Owner 获得权限后，旧 Owner 是否仍可迟到写入。

例如：

LeaseOwner = Agent B

Agent A still holds old token

如果 Effect Gateway 仍接受旧 Token，即使 Lease 本身正确运行，也可能发生迟到写入。

精确性质应是：

受保护写入必须使用当前有效的资源授权代际信息，旧 Owner 在新 Ownership 生效后不能继续产生新 Effect。

十五、Fencing Token 与 Safety Epoch：两种代际约束必须区别建模

Safety Epoch 界定某个安全控制域的授权时代。发生 Containment 或关键安全状态切换后，旧授权不应继续用于新的受保护操作。

Fencing Token 常用于资源所有权和 Lease，防止旧持有者迟到写入。

两者不能简单合并。

runtime:
  safety_epoch: 12

resource:
  resource_id: POST-100
  fencing_token: 57

某次操作需要同时满足：

Current Safety Epoch
AND
Current Resource Fencing Token

前者控制安全授权代际，后者控制具体资源所有权代际。

形式化验证能够帮助发现哪些转换必须同时校验多个独立代际。

十六、Policy Conflict Verification：冲突不是简单把 Deny 放在前面

第（四十四）篇建立了 Constitutional Policy、Domain Policy 和 Emergency Override。

但组合复杂：

P1: Containment prohibits writes.
P2: Recovery permits restoration.
P3: Break-glass grants emergency access.
P4: Root policy prohibits unaudited actions.
P5: Resource policy requires current lease.

如果简单使用 Deny Overrides Permit，P1 可能永久阻止 Recovery。

如果增加 Emergency Permit Overrides Deny，又可能过度放宽控制。

更好的设计是把 Emergency Recovery 定义为独立、范围化、可验证的动作，而不是给普通写权限增加例外。

例如 NormalWrite 和 RestoreApprovedConfiguration 应当是不同 Action。

后者仍要求有效 Incident、独立审批、指定 Resource、批准的 Restore Artifact、短期 Capability、当前 Safety Epoch 和 Effect Verification。

这样可以明确检查：

NormalWrite is denied.

AuthorizedRecovery may proceed.

而不是通过粗糙的统一优先级解决所有冲突。

十七、对第（四十四）篇 Conflict Resolution 的重要强化

如果把 Containment Deny 设计为绝对禁止所有写入，恢复将无法进行。

如果 Emergency Override 可以覆盖所有 Containment，事故隔离又可能被突破。

不能只依赖：

Emergency > Domain Deny

证明系统安全。

更稳健的模型应定义：

Constitutional Hard Constraints
        ↓
Containment-specific Action Rules
        ↓
Recovery Action Eligibility
        ↓
Emergency Capability Verification
        ↓
Resource / Effect Constraints
        ↓
Final Authorization Decision

策略组合时，应先定义每类 Action 的完整允许条件，而不只是给所有 Policy 排统一优先级。

十八、死锁：所有人遵守规则，却没有人能够继续

Research Agent 持有 Source Registry 的 Lock。

Fact Check Agent 等待 Lock 释放。

Research 又等待 Fact Check 完成，才能结束任务。

Research waits for Fact Check

Fact Check waits for Research Lock

类似问题也可能发生在：

Publisher 等待 Approval。

Approval 等待 Evidence。

Evidence 等待 Resource Lock。

Resource Owner 等待 Publisher 完成。

需要区分：

Deadlock：系统没有能够推进的动作。

Livelock：系统持续执行动作，却始终无法完成业务目标。

例如两个 Agent 不断释放和重新申请 Lease，但始终无人完成工作。

不能因为日志一直刷新，就认为系统取得进展。

十九、Recovery Liveness：恢复机制也可能成为阻塞源

第（四十一）篇 Recovery Proof、第（四十四）篇 Root Recovery Quorum 单独都合理，但可能组合成循环：

Recovery requires valid Policy.

Policy activation requires quorum.

Quorum requires trusted identities.

Trusted identity restoration requires
Recovery Authority.

Recovery Authority cannot activate
until Policy is restored.

这属于治理控制面的循环依赖。

必须建立 Recovery Liveness Verification。

先问：从某事故状态出发，是否存在合法恢复路径？

再问：在明确调度、公平性和外部可用性假设下，系统是否最终沿合法路径恢复或进入终止处置？

Recovery path exists.

与：

Recovery eventually occurs.

不是一回事。

存在可恢复路径，不等于系统必然恢复。

二十、Liveness 应区分“必然成功”和“必然有明确结果”

WordPress、Cloudflare、GitHub Actions、外部事实源和人工审批，都不由我们完全控制。

因此把所有 Liveness 定义为 Eventually SUCCESS 并不现实。

更合理的候选性质是：

Every accepted high-risk workflow
eventually reaches a terminal decision,
under stated availability and fairness assumptions.

终止结果可以是：

VERIFIED_COMPLETED
REJECTED
CANCELLED
FAILED_AND_RECONCILED
ESCALATED

Liveness 不要求所有业务操作成功，而要求系统在指定前提下取得可解释的最终结果。

例如 WordPress 超时后，不应永远 RUNNING 并不断重试。

应进入 EFFECT_RECONCILIATION，核验外部状态，再决定继续、停止或升级。

二十一、Model Checking 与普通 CI 测试有何不同？

普通 CI 测试通常使用预定义输入，例如 test_publish_without_approval，预期返回 DENY。

Model Checking 则探索模型允许的多种状态组合及转换顺序：

Approval → Edit → Containment → Recovery → Publish

Approval → Containment → Edit → Recovery → Publish

二者不是替代关系。

常规测试用于核验实现代码是否符合具体预期。

模型检查用于探索规范层面是否存在遗漏的行为路径。

最终应连接：

Formal Model
      ↓
Verified Properties
      ↓
Counterexample Traces
      ↓
Implementation Test Cases
      ↓
CI Regression Tests
      ↓
Runtime Verification

形式化模型寻找设计中的逻辑缺陷，工程测试核验实现是否忠实执行设计。

二十二、Counterexample-driven Governance：反例比抽象 PASS 更有价值

假设模型检查发现：

Invariant Violated:
NoStaleAuthorization

单独一个名称，价值有限。真正有用的是反例：

State 0:
Policy Version = 7
Safety Epoch = 12
Capability Issued

State 1:
Containment Activated
Safety Epoch = 13

State 2:
Recovery Started
Agent Returns to READY

State 3:
Old Capability Reused
Capability Epoch = 12

State 4:
Production Effect Executed

这里的缺陷是：Recovery 转换恢复了业务执行资格，却没有重新核验旧 Capability 是否适用当前 Epoch。

反例可转化成工程修复任务：

BLOCKER:
Effect Gateway must reject
capability_epoch != current_epoch.

进一步转化成回归测试：

stale_capability_after_recovery

Counterexample 不应只保存在检查报告，而应进入生产测试、Policy 和事故知识库。

二十三、Model Checking 不会自动证明模型与真实系统一致

假设模型验证了：

Every Publish action checks
the current Safety Epoch.

但真实生产还存在一个未经建模的旧发布接口，能够直接调用 WordPress。

即使模型检查通过，也无法阻止该接口绕开模型中的执行边界。

这是 Model–Implementation Gap。

要区分：

Specification Correctness：模型是否满足指定性质。

Implementation Conformance：真实实现是否满足规范中的协议和动作约束。

Environment Assumption Validity：身份、数据库、Gateway、WordPress 和调度机制是否满足模型前提。

模型检查通过，只意味着在已建立模型、所设假设下，已检查性质得到相应验证结果。

二十四、Refinement：从抽象状态机连接真实代码

形式化模型可能只包含一个 Publish 动作。

真实实现却是：

Validate Request
→ Load Approval
→ Check Policy
→ Acquire Lease
→ Call WordPress
→ Store Effect Receipt
→ Read Back Post

因此需要建立 Refinement Mapping，明确低层实现对应的抽象行为。

这只是项目级映射。真正的数学精化证明需要更严格的规范和推理。

但映射表已经帮助团队识别：模型中的安全前置条件，究竟在真实代码里由哪个组件负责？

二十五、TLA+、PlusCal、Alloy、Apalache 分别适合什么？

TLA+ / TLC

TLA+ 很适合描述分布式系统的状态、动作、并发和时序性质。TLC 能针对有限实例探索状态，并检查不变量与适用时序性质。

适合研究：

Containment
Recovery
Lease
Authorization
Effect Reconciliation

官方资料：https://github.com/tlaplus/tlaplus

PlusCal

PlusCal 用接近算法流程的表达方式描述并发程序，再转换为 TLA+ 规范进行分析。它可以降低部分建模门槛，但仍需理解 TLA+ 的状态与时序语义。

Alloy

Alloy 以关系建模见长，Analyzer 能在指定有限范围内寻找满足约束的实例或违反断言的反例。Alloy 6 支持时间相关状态建模。

适合：

Authority Graph
Delegation
Policy Scope
Governance Quorum
Role Conflict

官方资料：https://alloytools.org/

Apalache

Apalache 是针对 TLA+ 的符号模型检查器，使用 SMT 技术，支持有界模型检查、归纳不变量等方法。

TLC 与 Apalache 应按模型、语法兼容性和验证目标选择，不能简单认为其相互替代。

官方资料：https://apalache-mc.org/

项目可以先选一个关键状态机，通过 TLA+ / TLC 建立首个可重复的检查流程，再评估是否引入 Alloy 或 Apalache。

二十六、状态空间爆炸：为什么不能把所有 Agent 放进一个模型？

假设有 5 个 Agent，每个都有 6 种状态，不计其他变量，组合可能达到：

6 × 6 × 6 × 6 × 6
= 7,776

再加 Policy Version、Safety Epoch、Lease、Approval、Evidence、Break-glass 和 Effect Count，状态空间会迅速膨胀。

因此需要抽象。

例如不放完整文章，而只放：

ArtifactDigestMatched:
TRUE / FALSE

不放真实设备参数，而是：

CriticalEvidence:
VERIFIED / UNKNOWN / CONTRADICTED

这样可以集中研究真正影响安全决策的变量。

抽象必须以威胁模型、系统约束和事故经验为依据，不能只是为了让模型检查器更快。

二十七、完整案例：双重审批、紧急恢复和资源所有权怎样造成死锁？

网站因错误配置出现大规模 noindex，Containment 关闭普通写权限。

Recovery Agent 申请紧急恢复，需要：

Break-glass = 2 approvals

第一人已批准。第二人属于 Platform Recovery Team，但该团队使用的身份服务也在事故中处于隔离状态。

规则要求：

No emergency capability
without complete quorum.

最终形成：

Recovery needs Break-glass.

Break-glass needs second approval.

Second approval needs identity recovery.

Identity recovery needs Recovery Capability.

单条规则合理，组合起来却构成循环依赖。

缺陷不是“审批太严格”，而是：

恢复路径依赖了正在等待恢复的同一控制面。

因此需要事先批准的独立恢复路径：

Trusted Recovery Identity
+
Preapproved Recovery Procedure
+
Independent Evidence Store
+
Restricted Emergency Capability

它仍必须保留可核验身份、范围和审计，而不是建立无限期超级权限。

二十八、Quorum 本身也需要 Liveness Verification

第（四十四）篇建立 2-of-3 Governance Quorum。

但假设三位批准人中一人离职，一人账户被冻结，另一人只能使用已故障的身份系统。

表面上仍是 2-of-3，实际上：

Available Approvers = 0

因此模型不仅应检查 Quorum Cannot Be Bypassed，还应检查：

在声明的故障假设和可用人员条件下，是否仍存在安全操作或恢复路径。

Quorum 必须与 Root Rotation、Emergency Recovery 和职责独立性一起设计。

二十九、Runtime Assurance：模型通过后为什么还需要生产监测？

因为 Policy、Agent、WordPress 插件、凭据、网络与工作流都可能变化。

可将部分形式化性质转换成运行时机制：

No publish without approval.
→ Effect Gateway approval check

Old Safety Epoch cannot write.
→ Capability Epoch check

Break-glass may not exceed scope.
→ Emergency request scope check

No duplicate effect for Intent.
→ Effect Ledger / Idempotency check

但必须区分：

Pre-effect Enforcement：产生效果前阻止违规。

Runtime Monitoring：观察执行是否满足可监测性质。

Post-effect Reconciliation：核验真实外部效果。

只能事后看日志的 Monitor，未必能够阻止错误发生。

三十、Runtime Monitor 最危险的问题：可能没有看见全部事件

假设：

Every production publish
must have a valid decision receipt.

Monitor 只观察 Gateway 日志。但某旧脚本仍可直接创建 WordPress 文章，绕过了被监测的路径。

Dashboard 可能显示：

Policy Violations:
0

这并不代表整个网站没有违规发布，仅表示被观察到的事件未出现已知违规。

因此需要多个来源核验：

Gateway Effect Ledger
          ↕
WordPress REST State
          ↕
WordPress Revisions
          ↕
Deployment / Audit Records

发现 Unattributed Production Effect。

不完整的可观察性，不应产生完整的安全保证。

三十一、Counterexample 如何真正进入 Governance CI/CD？

建议建立 Formal Governance CI，不取代普通 CI，而是在高风险策略和状态机变更时增加形式化分析。

Policy / Workflow Change
           ↓
Formal Model Impact Analysis
           ↓
Relevant Model Selection
           ↓
TLA+ / Alloy Checks
           ↓
Counterexample Review
           ↓
Regression Test Generation
           ↓
Human Governance Review
           ↓
Deployment
           ↓
Runtime Conformance Monitoring

其中重要的是 Counterexample Review。

如果新 Policy 让旧模型出现反例，不能只修改测试期望值让 CI 变绿。

应分析：

反例是否揭示真实风险？

是否需要修改 Policy 或 State Machine？

是否需要更新原始 Governance Requirement？

如果是预期规则变化，是否获得对应权限级别的批准？

Formal CI 最终应该产生可供决策的证据，而不是仅仅一个 PASS。

三十二、将验证模型纳入 GitHub 仓库

对于现有 SEO Publisher，可以采用较小的目录：

governance/
├── models/
│   ├── publishing/
│   │   ├── SeoPublishing.tla
│   │   └── SeoPublishing.cfg
│   ├── containment/
│   │   └── ContainmentRecovery.tla
│   └── authority/
│       └── GovernanceAuthority.als
├── properties/
│   └── invariant-register.yaml
├── counterexamples/
│   └── regression-cases/
└── evidence/
    └── verification-manifests/

这是建议的目标目录，不表示生产仓库已经部署这些文件。

首先只建 SeoPublishing.tla，验证关键性质；模型稳定后，再将 Containment、Recovery、Governance Quorum 分别加入模型。

这比一次建设难以维护的巨大形式化平台更现实。

三十三、GitHub Actions 怎样执行最小模型检查？

TLA+ 官方工具链提供 TLC 命令行接口。

简化命令示意：

java -cp tla2tools.jar tlc2.TLC \
  -config SeoPublishing.cfg \
  SeoPublishing.tla

需要先取得版本固定、完整性可核验的 TLA+ 工具包，并配置适当 Java 环境。

实际命令、路径、配置应按工具版本验证。

CI 应保存：

Model Source Digest
TLC Version
Model Configuration
Checked Properties
State Coverage
Exit Status
Counterexample Artifacts

再根据实际结果决定是否阻断部署。

本文未实际运行该教学模型的 TLC 检查，也不声称已经得到真实 PASS。

正式集成时，应首先确认模型能解析、配置正确，并能发现预先注入的已知性质违规。

如果检查器连预期 Bug 都没有发现，不能直接相信其对生产模型的 PASS。

三十四、Formal Verification Result 也应成为 Evidence Artifact

此前建立了 AI Supply Chain、System-wide Safety Case、Policy Decision Receipt 和 Governance Decision Receipt。

现在需要新增：

Formal Verification Manifest。

verification_id: FV-045-001

model:
  name: SeoPublishing
  version: 1.0.0
  source_digest: sha256:<model-digest>

checker:
  name: TLC
  version: <validated-version>

configuration:
  file: SeoPublishing.cfg
  digest: sha256:<config-digest>

properties:
  - SafeEffect
  - NoStaleAuthorization
  - NoDuplicateEffect

assumptions:
  - bounded_workflow_instances
  - modeled_gateway_is_non_bypassable
  - trusted_evidence_input

result:
  status: NOT_YET_EXECUTED

evidence:
  report_ref: null
  counterexample_ref: null

这里使用 NOT_YET_EXECUTED 明确表示待验证模板。

真正执行后，必须按实际输出记录成功、失败、超时或未完成；不能把“工具运行结束”自动标记为“性质通过”。

Manifest 还应绑定：

Policy Version
Workflow Version
Gateway Version
Safety Epoch Semantics

否则模型验证的是旧逻辑，生产运行的可能已是另一个实现。

三十五、形式化验证不能只在 Policy 修改时运行

某些设计缺陷不来自 Policy 变更。

例如：

Resource Lease 实现变化。

Effect Gateway 新增批量发布功能。

Workflow State Machine 加入恢复状态。

Publisher 重试逻辑从三次改成五次。

这些变化即使没有修改 Rego，也可能影响真实行为。

因此建议使用 Impact-based Verification：

Change: Publisher Retry Logic
→ Check Effect Idempotency Model

Change: Lease Coordination
→ Check Resource Ownership Model

Change: Recovery Workflow
→ Check Recovery Safety / Liveness

Change: Root Delegation
→ Check Governance Authority Model

根据变更影响选择模型，避免每次低风险内容调整都重新执行全部形式化验证。

三十六、如何衡量 Formal Assurance 的真实价值？

只统计：

Formal Checks Passed: 100

意义有限。

100 次重复验证一个简单性质，并不代表系统获得全面安全保证。

建议监测：

这是项目建议指标，不是 TLA+、Alloy 或 NIST 规定的统一 KPI。

尤其需要重视 Counterexample Regression Rate。

发现的形式化问题应不断转化成工程控制。

三十七、真实 SEO/GEO 项目的分阶段实施

Phase 1：验证正式发布状态机

覆盖审批、内容 Digest、事实证据、Safety Epoch、一次性 Effect 和发布后对账。

Phase 2：加入故障和重试模型

模拟 WordPress 超时、API 成功但响应丢失、Worker 中断、重复请求、旧 Capability 重放。

重点发现重复发布与不确定 Effect 风险。

Phase 3：加入 Containment 与 Recovery

模拟授权撤销、旧 Epoch、Recovery Attestation、Read-only 到受限写入的权限恢复。

重点验证 Safety 与 Liveness。

Phase 4：加入多 Agent 资源并发

模拟两个 Agent 修改同一 Post、Lease 过期、旧 Owner 迟到写入、Fencing Token 冲突。

Phase 5：加入 Meta-Governance

模拟 Root Policy 更新、Dual Control、Quorum 不足、Break-glass、Emergency Override 和 Governance Recovery。

整个过程必须坚持：

从小模型开始，优先覆盖会造成真实生产风险的状态组合。

三十八、Game Day：把反例用于生产前演练

将第（四十）篇的 Game Day 进一步升级为：

Counterexample-driven Game Day。

例如模型发现：

Approval
→ Edit
→ Recovery
→ Publish

可能绕过重新审核。

那么 Game Day 应故意创建已审核文章、审核后修改、模拟 Containment、恢复 Publisher，再尝试正式发布。

检查 Gateway 是否真正拒绝旧 Approval。

如果模型发现：

Lease Expired
→ New Owner Granted
→ Old Owner Writes

可能发生重复修改，就在测试环境模拟迟到请求与并发写入。

这种方式比单纯固定健康检查更有针对性。

它把形式化模型发现的设计缺陷转化为测试真实实现的实验。

三十九、必须明确 Formal Methods 的四个边界

第一，模型可能遗漏现实系统的重要状态。旧发布接口如果没进入模型，模型无法自动发现它绕过执行控制。

第二，Model Checking 受到状态空间、建模抽象和工具能力限制。有限模型没有反例，不等于所有现实情况都没有反例。

第三，Liveness 依赖调度与外部环境假设。现实不满足 Fairness 或可用性前提时，模型结论可能不再适用。

第四，模型正确不等于实现正确。仍需要工程测试、生产监测、身份验证、证据核验和外部效果回读。

Formal Methods 是可信自动化的重要证据来源，不是替代所有其他控制的一次性认证。

四十、从 Model Checking 进入 Continuous Formal Assurance

此前治理体系已形成 Continuous Evaluation、Continuous Authorization、Continuous Policy Compliance 和 Continuous Runtime Monitoring。

现在进一步提出：

Continuous Formal Assurance。

核心不是每天重复运行同一模型，而是：

System Design
       ↓
Formal Specification
       ↓
Model Checking
       ↓
Counterexample Analysis
       ↓
Policy / State Machine Correction
       ↓
Regression Testing
       ↓
Production Deployment
       ↓
Runtime Monitoring
       ↓
Incident Evidence
       ↓
Model Refinement

真实事故持续反馈给模型，反例持续进入测试，策略与实现变化持续触发相关验证。

Formal Methods 不再只是上线前的一份独立报告，而成为长期治理体系的一部分。

这也是本项目“研究—实施—发布—监测—优化—知识沉淀”长期闭环的工程延伸。

---

结语：治理系统真正成熟，是能够主动寻找自己的失败路径

第（三十九）篇要求 Agent 持续证明行为可信。

第（四十）篇要求失控 Agent 能够被隔离和停止。

第（四十一）篇要求事故恢复后重新获得权限必须有证据。

第（四十二）篇发现多个 Agent 局部 PASS 不自动构成全局可信。

第（四十三）篇把治理规则放到真正的生产执行边界。

第（四十四）篇继续约束谁有资格制定、修改和紧急绕过治理规则。

第（四十五）篇面对更根本的问题：

即使各个机制都正确，它们组合以后是否仍然正确？

复杂系统的失败并不总是来自明显错误的组件。

Policy 正确、Lock 正确、Approval 正确、Containment 正确、Recovery 也正确，但执行顺序、状态交互和隐藏依赖，可能让这些机制组合成不正确结果。

因此不仅要问：

有没有规则？规则是否被执行？每条规则是否单独通过测试？

还必须问：

是否存在某种合法执行顺序，使系统最终突破了不应该突破的边界？

是否存在某种状态组合，使所有组件正常运行，却没有一条合法路径推动系统恢复？

Formal Methods 的价值在于精确描述系统、主动寻找反例，让一些本来只能在生产事故中发现的问题有机会在部署前暴露。

但也必须承认模型边界，持续核验模型与真实实现的关系。

最终生产级自治系统需要：

Formal Specification
          ↓
Safety Verification
          ↓
Liveness Verification
          ↓
Policy Conflict Analysis
          ↓
Counterexample Discovery
          ↓
Implementation Conformance
          ↓
Runtime Assurance
          ↓
Incident-driven Model Refinement

真正值得信任的 AI Agent 系统，不仅应该说明自己为什么正确，还应该系统性寻找自己在哪些条件下可能错误。

从第（四十四）篇的 Governance-governed Autonomous System，推进到：

Formally Specified and Runtime-Assured Autonomous System。

A governance system is not reliable merely because its individual rules are correct. Its state transitions, rule interactions, and recovery paths must also be verified.

治理系统不能只证明每条规则正确，还必须验证规则组合、状态转换和恢复路径是否仍然正确。

---

官方技术依据与研究边界

1. TLA+ / TLC — 官方项目

TLA+ 用于描述并发与分布式系统的状态和行为。TLC 是其主要模型检查工具之一，可以探索有限状态模型、检查不变量和适用的时序性质，并在违反时输出反例。

https://github.com/tlaplus/tlaplus

https://github.com/tlaplus/tlaplus/blob/master/USE.md

2. TLA+ 官方学习资源

本文对 Safety、Liveness、Fairness 与 Temporal Properties 的讨论参考了相应学习资料。

https://docs.tlapl.us/learning:start

https://www.learntla.com/core/temporal-logic.html

3. Alloy / Alloy Analyzer

Alloy 支持关系建模和有限范围分析，适合探索权限关系、委托结构、角色冲突等。Analyzer 可寻找违反断言的反例。

https://alloytools.org/

https://alloytools.org/spec.html

4. Apalache — Symbolic Model Checker for TLA+

Apalache 使用 SMT 技术分析 TLA+ 规范，支持有界模型检查、归纳不变量等方法，需核对适用特性及工具限制。

https://apalache-mc.org/

https://apalache-mc.org/docs/apalache/index.html

5. TLA+ 官方示例

官方 TLA+ 示例仓库提供经过维护的模型及配置。

https://github.com/tlaplus/Examples

本项目原创工程设计

以下概念为本项目针对 SEO/GEO 自动化提出或组合的工程模型：

• SEO/GEO Formal Governance Model
• Publishing State Machine Verification
• Cross-Agent Safety Invariant Registry
• Recovery Liveness Verification
• Policy Conflict Verification
• Counterexample-driven Governance
• Formal Verification Manifest
• Impact-based Formal Governance CI
• Model–Implementation Conformance Mapping
• Counterexample-driven Game Day
• Continuous Formal Assurance
• Formally Specified and Runtime-Assured Autonomous System

这些机制适合继续转化为项目 Schema、模型、测试、验证 SOP 与生产控制，但不能表述为 TLA+、Alloy、Apalache、NIST 或 Google 已发布的统一 SEO/GEO Agent 治理标准。

---

第（四十六）篇预告：Runtime Assurance Architecture——形式化验证之后，怎样让生产系统持续满足被验证的约束？

第（四十五）篇解决了：

怎样在状态模型中系统性寻找危险路径与不可恢复状态？

但 Model Checker 验证的是模型，生产运行的是代码。

如果模型已通过检查，但实际 Cloudflare Worker、WordPress Publishing Gateway、Effect Ledger 或 Agent Workflow 在运行中偏离模型，该怎么办？

下一篇建议进入：

Runtime Assurance Architecture / Model–Implementation Conformance / Runtime Monitor Synthesis / Safety Envelope / Shielded Execution / Verified Controller / Fallback Controller / Online Conformance Checking / Continuous Attestation / Assurance Drift / Runtime Recovery

目标架构：

Verified Formal Model
          ↓
Executable Runtime Contract
          ↓
Runtime Conformance Monitor
          ↓
Safety Envelope
          ↓
Authorized Controller
          ↓
Protected Production Effect
          ↓
Observed State Reconciliation
          ↓
Continuous Assurance Evidence

继续回答：

如何确保形式化验证的结论，不会在真实 Agent 生产运行中逐渐失效？

从 Formally Specified and Runtime-Assured Autonomous System 进入 Continuously Monitored and Runtime-Enforced Autonomous System。