Repository navigation
🤖 tests: add a TLA+ check of the CoderAIGatewayKey key lifecycle and a KIND verify skill - #391
Conversation
Change-Id: I4b4fb8a81e4b365932719c88bb8fdd69a0d13c73 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Add hack/formal/aigatewaykey: a TLA+ model of the key issue, Secret write, retire, orphan sweep and delete steps, and check.sh, which reads the guard statements and timing constants from the Go source, fingerprints the covered functions, and runs TLC 1.7.4 (pinned by SHA-256). The project skill verify-aigatewaykey-model says when and how to run it and how to read a result. Rules: SecretKeyAlive and NoLeakAfterRelease. Both hold at the quick bound (18.6M states) and the deep bound (209M states). --config stall shows a leak when the process pauses between the create marker and the create request. Signed-off-by: Thomas Kosiewski <tk@coder.com> --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_ Change-Id: I83211a19f5c633d93096d28bddd1b5cccb0b640d
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
Security findingsAdvisory findings (3)
ℹ️ 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. |
|
@codex security review |
![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: 717db990d3
ℹ️ 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".
There was a problem hiding this comment.
🛡️ Codex Security Review
Here are some automated security review suggestions for this pull request.
Reviewed commit: 717db990d3
ℹ️ 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.
- verify.sh: never default VERIFY_BASE to /tmp; refuse base, bin and run dirs that another user can write before PATH use or sourcing run.env. - verify.sh doctor: require all 7 aggregated resources in discovery. - coderprovisioner journey: set organizationName coder. - check.sh: exit 2 when the TLC download fails; report functions that left the covered list as STALE. Change-Id: Ia29f4e67ca9c9d4a1a9aeb38a337f7bb8679855f Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3b647f2dc5
ℹ️ 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".
There was a problem hiding this comment.
🛡️ Codex Security Review
Here are some automated security review suggestions for this pull request.
Reviewed commit: 3b647f2dc5
ℹ️ 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.
- Refuse run and base dirs with an ancestor that another user owns, or can write without the sticky bit; default the run dir away from /tmp. - Bind cleanup and the ownership check to the node container ID. - Count untracked files in SOURCE_DIRTY. - Refuse attached -s server overrides. Change-Id: Ib2e1c3a0d97cb227342aa6b21d00195cb1519bd1 Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
There was a problem hiding this comment.
🛡️ Codex Security Review
Here are some automated security review suggestions for this pull request.
Reviewed commit: 23cf66db56
ℹ️ 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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 23cf66db56
ℹ️ 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".
- check.sh: run TLC from a private, re-verified copy of tla2tools.jar; exit 2 when the output folder cannot be used. - verify.sh: require absolute dirs; launch only into a new or empty run dir. Change-Id: If5900ab04c484b459e07ac2d6cb9b57e74d45daf Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
🛡️ 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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d8e05b26a6
ℹ️ 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".
Summary
Adds two project skills that let an agent prove changes to coder-k8s.
verify-coder-k8slaunches the real operator on a disposable KIND cluster with a real Coder and drives the CRDs and the aggregated API throughkubectl.verify-aigatewaykey-modelmodel-checks theCoderAIGatewayKeykey lifecycle with TLA+, against guard statements and timing constants thatcheck.shreads from the Go source. The PR changes no product code.Background
A
CoderAIGatewayKeykeeps a full-trust Coder AI Gateway key in a Secret. Its safety depends on step order across reconciles that can stop at any step, a lagging informer cache, and requests that land after the operator gave up on them. Unit tests rarely reach those interleavings. The repo also had no single scripted way to launch the operator plus Coder and capture proof of a user-facing change.Implementation
hack/formal/aigatewaykey/AIGatewayKey.tla: a model of one object and one controller. It covers the issue step (cleanup record, marker, create, Secret write loop), adopt and recover, the orphan sweep, the retire step, and the delete path. It also covers late Coder commits, late Secret writes, resourceVersion conflicts, crashes, and actions by a person.hack/formal/aigatewaykey/check.sh: reads 10 guard facts and 6 constants from the Go source and fingerprints the 30 covered functions. It then runs TLC 1.7.4 (pinned by SHA-256). Exit codes: 0 pass, 1 violation, 2 cannot run, 3 STALE (covered code changed since the last review).hack/formal/aigatewaykey/view.mjs: a/statechartview that labels states and steps in operator words..mux/skills/verify-aigatewaykey-model/SKILL.md: when to run the check, the coverage table, how to read a result, and how to update the model..mux/skills/verify-coder-k8s/:scripts/verify.sh(launch,doctor,kubectl,node,coder-api,capture,collect,cleanup), a throwaway Postgres manifest, and a feature map of 5 user journeys.Rules checked:
SecretKeyAlive: while the object exists, the Secret never holds a key that Coder no longer has, unless a person deleted it.NoLeakAfterRelease: when the finalizer goes, Coder has no key of the object and no create can still commit.Validation
deleteOwnKey.check.shexited 1, and/statechartgave a 27-step path to the deleted key. With the line restored, the check passed with exit 0.verify-coder-k8s: a full run from launch to cleanup passed in about 2.7 minutes. It covered launch, doctor, theCoderControlPlanejourney, and theCoderTemplate/CoderWorkspacejourney checked through the Coder API. Cleanup left no cluster, container, or image tag behind.Known finding (not fixed here)
check.sh --config stallfailsNoLeakAfterRelease. Nothing bounds the time between the create marker (attemptStartinissueKey) andCreateAIGatewayKey, the wayaiGatewayKeyMaxWriteAgebounds Secret writes. A leader that freezes for about 5 minutes and then sends the create can commit a key after the delete path has already released the object. The docs do not list this assumption. I did not reproduce it live.Risks
Low. The PR adds files under
.mux/skills/andhack/formal/only. No build, CI job, or product code path reads them.Generated with
mux• Model:anthropic:claude-opus-5-5• Thinking:high• Cost:$10.77