[ThomasK33]

Why

The operator's goal is to land the open lifecycle issues he filed. This PR closes #222, the follow-ups from the review of #221.
Three edits to the destroy proof broke no rule of the lifecycle model. Only the coverage hash flagged them: a capture that keeps the host's autogroup, a readProvenProgramGroup that returns no record, and an isProgramGroupAlive that reads an unproven group alive.

What changed

• Two new model guards. TokenNamesProgram turns FALSE when captureToken can keep the host's autogroup. Its mutant breaks R16: destroy records destroyed while the group runs. ReusedIdReadsGone turns FALSE when an unproven group reads alive. Its mutant shows that no wait of destroy passes while an unrelated group holds the id, through the new witness WitnessWaitPassesReusedId.
• DestroyStopsLeftovers now also reads readProvenProgramGroup and hasToken.
• Unit tests for a refused /proc/<pid>/task listing and for a capture that still reads the host's autogroup. docs/USAGE.md names an empty or malformed autogroup file, and the host's kill without a token. Limit 2 now says that a kill without the check can reach an unrelated process that took the group id. A new limit 6 names the two declined cases: an idle time-out whose check cannot run records exited while a leftover runs (a later destroy fails with HOST_TIMEOUT, and gc can remove the folder), and under hidepid a destroy that cannot prove a hidden group gone fails with HOST_TIMEOUT.

Scope

No product code changes. The issue's other items stay as they are, for these reasons:

• (a) An idle exit whose check cannot run records exited with a leftover. That is the same state as a program that exits on its own and leaves a process, which USAGE limit 5 covers. Making gc check groups would be a new feature.
• (b) Under hidepid=2, destroy reads a hidden group alive and times out. That is the fail-safe side: the hidden process can also be a sudo child of the session. Live hidepid tests need a root /proc mount, which this host cannot do.
• (c) An unreadable boot id stays unknown. With unproven, destroy would record destroyed while the proven group can still run.

Verification

• .agents/skills/verify-session-lifecycle/scripts/check.sh --update-coverage: exit 0, 55 runs as expected, 5,042,251 and 5,218,828 distinct states.
• A script breaks each guarded line in a copy of the code: 5 of 5 breaks turn their guard FALSE on this branch, 0 of 5 on main.
• Unit 1595 passed. Each new unit test fails when the code line that it covers is broken.

Closes #222

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: xhigh

[ThomasK33]

@codex review

[ThomasK33]

@codex security review

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-11-02T18:45:29.862025Z	4599f01	Manual request
🔒 Security Review	✅ Completed 2026-11-02T18:45:26.091642Z	4599f01	Manual request

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Can't wait for the next one!

Reviewed commit: 366ca52b0b

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 366ca52b0b

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[ThomasK33]

@codex review

[ThomasK33]

@codex security review

[chatgpt-codex-connector]

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 4599f01ba9

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. 🚀

Reviewed commit: 4599f01ba9

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".