用途
verify-execution-lease 用于对智能体（agent）运行时的执行租约（execution lease）与持久化步骤日志进行形式化验证。它借助 TLA+ 建模单轮的执行租约、其各次运行，以及一个持久化的执行步骤，并由 TLC 在“三个运行”的边界内进行穷尽检查。该工具应在修改租约的申领、续订、释放、栅栏写入、回收器（reaper）等相关逻辑时使用。
主要能力
模型守护以下承诺与不变量：
- P8：对于重放策略为 never 的步骤，其外部效果在至多一次的意义上执行（across every run and lease generation），包括被废黜却仍在运行的 worker。若该性质被破坏，崩溃或接管后邮件或非幂等写入可能被重复发送。
- P1：只有当前有效租约代际的所有者才能向
agent_execution_steps提交写入。 - P6（不允许复活） 与 ClaimRespectsLiveOwner 用于守护租约本身。
P8 是针对每个步骤行的；它假设每次调用重试都到达同一个步骤 id，而重新规划的调用是否如此由工具调用日志负责，该模型不覆盖这部分（见 NOTES.md 的“Outside the model”）。
verification/execution-lease/NOTES.md 记录了假设、边界、未覆盖内容、结果、已知发现以及代码到模型动作的映射。
使用方式
运行命令：
pnpm verify:execution-lease
需要 Java 11 或更新版本（例如 brew install openjdk@21，或 PATH 中任意可用的 java）。首次运行会把锁定版本的 TLA+ 工具下载到 .tmp/tla/ 并校验其 sha256。
一次约 3 至 5 分钟；--quick 只运行两项检查，约 2 至 3 分钟。
退出码含义：
- 0：所有检查通过、所有变异仍失败、所有已知发现仍可复现，且没有受覆盖函数发生变更。
- 1：上述某项不成立，输出会指明是哪一项。
- 2：无法运行（没有 Java、工具未校验通过、TLC 错误）。绝不可将退出码 2 视为通过。
当改动触及被覆盖代码时：manifest.json 列出了被覆盖代码及每个条目的哈希（记录于 coverage.syncCommit），包括具名函数和锚定区域（由精确的 from/to 字符串界定，用于大闭包内的逻辑）。若编辑了其中一项，运行器会以“covered code changed”失败；若锚点不再恰好匹配一次，则以退出码 2 结束，直到更新锚点。此时应在 NOTES.md 的映射中找到该函数对应的模型动作并重读两者；若协议改变，应修改动作以匹配代码，保持每个真实事务对应一个动作、守卫条件等于代码的 WHERE 子句与检查，并确保引用的 file:line 保持最新。然后运行 pnpm verify:execution-lease；只有在模型已描述新代码后，才运行 pnpm verify:execution-lease --update-coverage 来移动同步提交。
失败解读
ExecutionLease.cfg 或 ExecutionLeasePolicyFlip.cfg 中的违规要么是真实缺陷，要么是建模错误。应参照所引代码逐步走查 TLC 轨迹：若每一步都是代码可能执行的操作，则为缺陷，需用代码原话按编号序列报告；若某一步在代码中不可能，则修正该动作的守卫以匹配代码。不得为通过而弱化 P8、P1、P6 或 ClaimRespectsLiveOwner，不得删除变异，也不得缩小边界。若某个变异不再失败，说明该检查失去了捕获该破坏的能力，应先修正模型。
适用场景与限制
适用于对智能体执行租约、栅栏写入与持久化步骤日志的并发与崩溃一致性进行模型检查，尤其适合在修改租约申领、续订、释放、回收器等逻辑时作为回归验证。限制包括：P8 按步骤行建模，且假设重试到达同一步骤 id，不覆盖工具调用日志负责的重新规划调用是否如此；检查在固定边界（三个运行）内进行；运行依赖 Java 与首次下载的 TLA+ 工具；退出码 2 不可视为通过。已知发现存放于 findings/，其中的配置可复现当前代码的真实缺口（F2、F3；F1 与 F4-F6 为读代码得出的发现），它们预期失败；当某项被修复后，运行器会报告其不再复现，此时应把对应配置移入 manifest.json 的 checks 并更新 NOTES.md。