Release v0.2.8 with Rust 1.99.1

.agents/skills/taskmgr-verify-processes/Processes-broken.cfg

@@ -0,0 +1,4 @@
+CONSTANT Broken = TRUE
+INIT Init
+NEXT Next
+INVARIANT Safety

.agents/skills/taskmgr-verify-processes/Processes.cfg

@@ -0,0 +1,4 @@
+CONSTANT Broken = FALSE
+INIT Init
+NEXT Next
+INVARIANT Safety

.agents/skills/taskmgr-verify-processes/Processes.tla

@@ -0,0 +1,57 @@
+---- MODULE Processes ----
+EXTENDS Naturals, Sequences, FiniteSets
+CONSTANT Broken
+VARIABLES phase, generation, handle, applied
+vars == <<phase, generation, handle, applied>>
+
+Init ==
+    /\ phase = "Selected"
+    /\ generation = 1
+    /\ handle = 0
+    /\ applied = 0
+
+Confirm ==
+    /\ phase = "Selected"
+    /\ phase' = ("Queued")
+    /\ UNCHANGED <<generation, handle, applied>>
+
+ReusePid ==
+    /\ handle = 0 /\ generation = 1 /\ phase \in {"Selected", "Queued"}
+    /\ generation' = (2)
+    /\ UNCHANGED <<phase, handle, applied>>
+
+OpenProcess ==
+    /\ phase = "Queued"
+    /\ handle' = (generation)
+    /\ phase' = ("Opened")
+    /\ UNCHANGED <<generation, applied>>
+
+CheckCreationTime ==
+    /\ phase = "Opened"
+    /\ phase' = (IF Broken \/ handle = 1 THEN "Verified" ELSE "Failed")
+    /\ UNCHANGED <<generation, handle, applied>>
+
+Apply ==
+    /\ phase = "Verified"
+    /\ phase' = ("Applied")
+    /\ applied' = (handle)
+    /\ UNCHANGED <<generation, handle>>
+
+ApiFailure ==
+    /\ phase = "Verified"
+    /\ phase' = ("Failed")
+    /\ UNCHANGED <<generation, handle, applied>>
+
+Close ==
+    /\ phase \in {"Selected", "Queued"}
+    /\ phase' = ("Cancelled")
+    /\ UNCHANGED <<generation, handle, applied>>
+
+Done ==
+    /\ phase \in {"Applied", "Failed", "Cancelled"}
+    /\ UNCHANGED <<phase, generation, handle, applied>>
+
+Next == Confirm \/ ReusePid \/ OpenProcess \/ CheckCreationTime \/ Apply \/ ApiFailure \/ Close \/ Done
+
+Safety == applied # 2
+====

.agents/skills/taskmgr-verify-processes/SKILL.md

@@ -0,0 +1,46 @@
+---
+name: taskmgr-verify-processes
+description: "检查 TaskManagerRust 结束进程：按创建时间核对，再使用同一已打开句柄的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。"
+---
+
+# 结束进程：按创建时间核对，再使用同一已打开句柄
+
+保证：只有创建时间与保存身份匹配的进程句柄才会交给操作。
+
+破坏后的用户影响：否则 PID 复用可能导致结束或修改另一个进程。
+
+## 源码与模型对应
+
+同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。
+
+| 源码 | 模型边界 |
+| --- | --- |
+| `src/system/process_identity.rs` | open_process_for_identity |
+| `src/pages/processes/action_worker.rs` | open_action_process / execute_end / execute_set_priority |
+| `src/pages/processes/actions.rs` | apply_confirmed_affinity 的已验证句柄边界 |
+
+模型：`Processes.tla`；正常配置：`Processes.cfg`；负例配置：`Processes-broken.cfg`；中文视图：`view.mjs`。
+
+## 运行
+
+先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录：
+
+```sh
+python3 verification/formal/verify.py processes --self-test
+```
+
+需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。
+
+当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。
+
+自检会在临时源码副本里跳过 open_process_for_identity 的创建时间比较。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。
+
+对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。
+
+## 范围与维护
+
+一个 PID、两个创建时间、一个进程句柄、一次操作；依赖 Windows 句柄固定进程对象的语义。适用于 handle-based 操作，不证明进程树全体原子性、亲和性位宽运算或线程快照完整性。
+
+TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。
+
+遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。

.agents/skills/taskmgr-verify-processes/view.mjs

@@ -0,0 +1,7 @@
+export const title = "结束进程 - 按创建时间核对, 再使用同一已打开句柄";
+const names = {"Selected": "选中进程并保存身份", "Queued": "确认操作，后台排队", "Opened": "打开目标的进程句柄", "Verified": "创建时间匹配，持有该句柄", "Applied": "操作已执行", "Failed": "目标变化或操作失败", "Cancelled": "操作未开始时关闭程序"};
+export const state = v => v.applied === 2 ? "误操作了复用后的进程" : v.phase === "Verified" && v.handle === 2 ? "身份检查被绕过，错误句柄被放行" : names[v.phase];
+const steps = {"Confirm": "确认结束进程", "ReusePid": "原进程退出，PID 被复用", "OpenProcess": "后台按 PID 打开进程", "CheckCreationTime": "比较保存与实际创建时间", "Apply": "使用核对后的同一进程句柄", "ApiFailure": "进程退出或系统调用失败", "Close": "关闭程序，取消尚未开始的请求", "Done": "保留执行结果"};
+export const step = a => steps[a] ?? a;
+export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程";
+export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"};

.agents/skills/taskmgr-verify-sampling/SKILL.md

@@ -0,0 +1,47 @@
+---
+name: taskmgr-verify-sampling
+description: "检查 TaskManagerRust 性能采样：缺失或无效数据不得画成真实零值的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。"
+---
+
+# 性能采样：缺失或无效数据不得画成真实零值
+
+保证：缺失容量、无效间隔或失败读数不能成为新增的真实零值历史点。
+
+破坏后的用户影响：否则图表会把未知或失败伪装成资源空闲。
+
+## 源码与模型对应
+
+同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。
+
+| 源码 | 模型边界 |
+| --- | --- |
+| `src/pages/gpu.rs` | record_memory_history / memory_percentage |
+| `src/pages/performance.rs` | apply_system_sample 的内存容量与历史门控 |
+| `src/pages/cpu.rs` | apply_system_sample 对 invalid delta 的历史与 stale 决策 |
+| `src/system/disk.rs` | 零间隔成功读取仅推进基线，不发布速率 |
+
+模型：`Sampling.tla`；正常配置：`Sampling.cfg`；负例配置：`Sampling-broken.cfg`；中文视图：`view.mjs`。
+
+## 运行
+
+先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录：
+
+```sh
+python3 verification/formal/verify.py sampling --self-test
+```
+
+需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。
+
+当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。
+
+自检会在临时源码副本里删除 record_memory_history 的缺失或零容量门控。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。
+
+对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。
+
+## 范围与维护
+
+一次发布决策、四种来源、一个既有历史点。CPU valid 标志与原生计数器计算视为输入；磁盘仅抽象零间隔分支；不证明 Win32 采样数值准确或所有溢出算术。
+
+TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。
+
+遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。

.agents/skills/taskmgr-verify-sampling/Sampling-broken.cfg

@@ -0,0 +1,4 @@
+CONSTANT Broken = TRUE
+INIT Init
+NEXT Next
+INVARIANT Safety

.agents/skills/taskmgr-verify-sampling/Sampling.cfg

@@ -0,0 +1,4 @@
+CONSTANT Broken = FALSE
+INIT Init
+NEXT Next
+INVARIANT Safety

.agents/skills/taskmgr-verify-sampling/Sampling.tla

@@ -0,0 +1,72 @@
+---- MODULE Sampling ----
+EXTENDS Naturals, Sequences, FiniteSets
+CONSTANT Broken
+VARIABLES phase, kind, eligible, history
+vars == <<phase, kind, eligible, history>>
+
+Init ==
+    /\ phase = "Ready"
+    /\ kind = "none"
+    /\ eligible = FALSE
+    /\ history = 1
+
+ChooseCpu ==
+    /\ phase = "Ready"
+    /\ phase' = ("Sampling")
+    /\ kind' = ("cpu")
+    /\ UNCHANGED <<eligible, history>>
+
+ChooseMemory ==
+    /\ phase = "Ready"
+    /\ phase' = ("Sampling")
+    /\ kind' = ("memory")
+    /\ UNCHANGED <<eligible, history>>
+
+ChooseGpu ==
+    /\ phase = "Ready"
+    /\ phase' = ("Sampling")
+    /\ kind' = ("gpu")
+    /\ UNCHANGED <<eligible, history>>
+
+ChooseDisk ==
+    /\ phase = "Ready"
+    /\ phase' = ("Sampling")
+    /\ kind' = ("disk")
+    /\ UNCHANGED <<eligible, history>>
+
+ValidSample ==
+    /\ phase = "Sampling"
+    /\ phase' = ("Candidate")
+    /\ eligible' = (TRUE)
+    /\ UNCHANGED <<kind, history>>
+
+MissingOrInvalid ==
+    /\ phase = "Sampling"
+    /\ phase' = ("Candidate")
+    /\ eligible' = (FALSE)
+    /\ UNCHANGED <<kind, history>>
+
+Publish ==
+    /\ phase = "Candidate" /\ (eligible \/ (Broken /\ kind = "gpu"))
+    /\ phase' = ("Fresh")
+    /\ history' = (history + 1)
+    /\ UNCHANGED <<kind, eligible>>
+
+ZeroDiskInterval ==
+    /\ phase = "Sampling" /\ kind = "disk"
+    /\ phase' = ("BaselineOnly")
+    /\ UNCHANGED <<kind, eligible, history>>
+
+RetainHistory ==
+    /\ phase = "Candidate" /\ ~eligible /\ ~(Broken /\ kind = "gpu")
+    /\ phase' = ("Stale")
+    /\ UNCHANGED <<kind, eligible, history>>
+
+Done ==
+    /\ phase \in {"Fresh", "Stale", "BaselineOnly"}
+    /\ UNCHANGED <<phase, kind, eligible, history>>
+
+Next == ChooseCpu \/ ChooseMemory \/ ChooseGpu \/ ChooseDisk \/ ValidSample \/ MissingOrInvalid \/ Publish \/ ZeroDiskInterval \/ RetainHistory \/ Done
+
+Safety == history > 1 => eligible
+====

.agents/skills/taskmgr-verify-sampling/view.mjs

@@ -0,0 +1,7 @@
+export const title = "性能采样 - 缺失或无效数据不得画成真实零值";
+const names = {"Ready": "保留上一轮可信曲线", "Sampling": "后台读取性能数据", "Candidate": "检查数据有效性", "Fresh": "追加真实采样点，包括真实零值", "Stale": "保持旧曲线，显示未知或未刷新", "BaselineOnly": "零间隔磁盘采样仅推进基线"};
+export const state = v => v.history > 1 && !v.eligible ? "未知容量被画成真实零值" : names[v.phase];
+const steps = {"ChooseCpu": "采样 CPU", "ChooseMemory": "采样物理内存", "ChooseGpu": "采样 GPU 显存", "ChooseDisk": "采样磁盘", "ValidSample": "读数及计算前提有效", "MissingOrInvalid": "数据缺失、容量未知或间隔无效", "Publish": "追加本次历史点", "ZeroDiskInterval": "磁盘读取成功但间隔为零，仅推进基线", "RetainHistory": "不追加伪造的零值", "Done": "等待下一次采样"};
+export const step = a => steps[a] ?? a;
+export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程";
+export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"};

.agents/skills/taskmgr-verify-services/SKILL.md

@@ -0,0 +1,46 @@
+---
+name: taskmgr-verify-services
+description: "检查 TaskManagerRust 服务重启：只有完成停止后才允许启动的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。"
+---
+
+# 服务重启：只有完成停止后才允许启动
+
+保证：重启成功必须经过确认停止和发起启动两个阶段。
+
+破坏后的用户影响：否则旧的 Running 状态会掩盖没有完成的重启。
+
+## 源码与模型对应
+
+同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。
+
+| 源码 | 模型边界 |
+| --- | --- |
+| `src/pages/services/model.rs` | restart_after_stop / stop_has_completed / classify_control_result |
+| `src/pages/services/sampler.rs` | restart_open_service / poll_service_stop |
+| `src/pages/services.rs` | start_worker |
+
+模型：`Services.tla`；正常配置：`Services.cfg`；负例配置：`Services-broken.cfg`；中文视图：`view.mjs`。
+
+## 运行
+
+先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录：
+
+```sh
+python3 verification/formal/verify.py services --self-test
+```
+
+需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。
+
+当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。
+
+自检会在临时源码副本里把 restart_after_stop 的非停止分支改成 Ok(state)。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。
+
+对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。
+
+## 范围与维护
+
+一个服务、一次重启、最多两个未停止观察。ticks 是有限观察预算，不是 30 秒时钟证明；SCM 调用可能阻塞、开始/关闭的跨线程竞争不在成功判定性质内。
+
+TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。
+
+遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。

.agents/skills/taskmgr-verify-services/Services-broken.cfg

@@ -0,0 +1,4 @@
+CONSTANT Broken = TRUE
+INIT Init
+NEXT Next
+INVARIANT Safety

.agents/skills/taskmgr-verify-services/Services.cfg

@@ -0,0 +1,4 @@
+CONSTANT Broken = FALSE
+INIT Init
+NEXT Next
+INVARIANT Safety