Repository navigation
chore: add the verify-native-lifecycle TLA+ skill - #24
Conversation
Adds a project skill that model-checks, with TLA+ and TLC, how the native addon keeps state across Node environments (the main thread and worker_threads Workers) and across one terminal's life. It checks four rules: createTerminal uses its own environment's class reference, loading never deletes another environment's reference, each handle is freed at most once, and no libghostty call reaches a freed or null handle. This check found the worker-thread crash that the previous commit fixes. The model describes the fixed code. Three mutant configs (the old static reference, DisposeNative without `terminal_ = nullptr`, and no use guards) must each break their rule, so every run shows that each rule can fail. Run: .agents/skills/verify-native-lifecycle/run.sh (about 20 s, needs Java 11+, downloads tla2tools v1.7.4 to vendor/ with a sha256 check). _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_ Change-Id: Iff1cda4aaa5bc6e98624787e0e5ed21d1adfa587 Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e7b67ed2e0
ℹ️ 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".
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
Change-Id: Ie78a8d38ccb368f4d3d5df8b7f3585ff8c5a018c Signed-off-by: Thomas Kosiewski <tk@coder.com>
… fix Explains how to read a TLC counterexample from the log when the agent does not have the pstack /statechart skill. Updates the model comment and the coverage record for the instance-data assertion in TerminalWrap::Init, and moves the sync commit to that change. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_ Change-Id: I0cf397b7723446c7de3a06eefba399c3b7b431ed Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. 🚀 Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
Adds
.agents/skills/verify-native-lifecycle/, a project skill that model-checks with TLA+ (TLC) how the native addon keeps state across Node environments and across one terminal's life.Rules it checks
CreateUsesOwnClasscreateTerminalin a thread uses the class reference that this thread made.LoadDeletesOnlyOwnRefHandleFreedOnceNoCallOnDeadHandleThe model found the worker-thread crash that the PR below this one fixes. It describes the fixed code. Each action in
model/AddonEnvLifecycle.tlanames the function it stands for, andSKILL.mdhas a coverage record and a sync commit.Each rule can fail
run.shchecks the current code and three mutants, and compares each result with an expected list:currentmutant-process-static(the code before the fix)CreateUsesOwnClass,LoadDeletesOnlyOwnRefmutant-dispose-keeps-pointer(noterminal_ = nullptrinDisposeNative)HandleFreedOncemutant-no-use-guards(no#assertUsable, noRequireTerminalnull check)NoCallOnDeadHandleRun
It takes about 20 seconds, needs Java 11 or later, and downloads tla2tools v1.7.4 to
vendor/tla2tools/with a sha256 check. Result here:OK: every result matches EXPECT.Bounds and limits
I proved the skill once on a scratch break: removing
terminal_ = nullptrfromDisposeNativemadeHandleFreedOncebreak, and the real build then segfaulted on GC afterdispose(). I dropped the scratch change afterwards.The sync commit names this stack's fix commit. After the fix squash-merges, I will move it to the squash commit on
main.Generated with
xum• Model:anthropic:claude-opus-5-5• Thinking:high