形式化建模（TetherFormal）

formal/lean 是一个独立的 Lake 工程，用 Lean 4 对 Tether 的核心语义做对照建模与机器检查证明。 它的目标是发现真实逻辑缺陷，不是写漂亮证明：疑似缺陷以最小反例（#eval/decide）写进 findings/ 报告，附 C# 文件与行号锚点。它与 运行期不变量互补——不变量在运行期看护两个可能分叉的事实， 形式模型在设计时穷举状态空间里的交错。

对应实现：formal/lean（不在 Tether.slnx 内）。

是什么，不是什么

• 是建模加证明：四个领域共 21 个模块、268 条 theorem，零 sorry/axiom/native_decide。
• 形式化的是抽象语义，不是 C# 代码本身：seq/offset 建模为 Nat、SHA-256 假设无碰撞； tracer、AsyncLocal、锁内部、task 收敛等实现细节被显式抽象掉。每个模块的文件头必须写明三件事： 对应的 C# 源文件与行/成员锚点、建模假设、抽象掉了什么。
• 不替代运行期不变量与测试：模型不执行产品代码，证明的是”这组规则在这组假设下自洽”； 运行期的看护仍由 Tether.Invariants 与 xunit 测试承担。

覆盖范围

findings：反例驱动的缺陷发现

findings/ 收录 13 份报告，每份含严重度、C# 位置、反例与处置状态（修复 / 有意设计不改）。 证明纪律规定模型 worker 只读 src/ 与 tests/，只在 formal/ 下写文件——修复永远发生在产品代码一侧。

几个已经反哺主线的例子（报告写就时修复尚在工作区，随后已合入 main）：

• F001 once 双触发：并发 dispatch 各自快照同一 once hook，仅靠摘除挡不住第二次调用—— 反例直接推动了 Events.cs 的原子认领（TryClaimOnce），即 Events 参考页记录的”比 dsh 更严格”的 once 语义。
• cordis stale pending missing：快照的 Missing 在部分依赖发布后不收窄，启动诊断会等一个 已发布的服务——对应 Registry 的 Missing 收窄修复。
• packages replaces claim TOCTOU：并发安装各自基于旧快照通过 replaces 认领检查、双双落锁—— 对应租约内复检权威判定的安装修复（见 插件项目的准入规则）。
• authz hooks ask downgrade：hook 的 ask 把内层 deny 降级为可批准的 ask——对应 “hook 与 guardrails 只收紧、不放宽内层决策”的授权修复（见 pi 移植指南的 pre-execute 语义）。

构建与运行

需要 elan 管理的 Lean 4 toolchain，版本固定在 lean-toolchain （当前 leanprover/lean4:v4.34.1）：

cd formal/lean
lake build

不引入 Mathlib，只用 Lean core 自带的 decide / simp / omega。工程当前不在 CI 里： .github/workflows 只跑 dotnet 构建/测试，lake build 是本地显式动作，提交信息以”全量 lake build 通过、无 sorry”为验收口径。