Repository navigation
Prune five examples whose ceremony costs more than the answer - #10
Merged
Merged
Conversation
…ugh composition separation-of-duties: a toxic-combination table checked by group name, and a role added later that approves; two grants, neither listed, make a conflict. scp-escalation: moving prod into an OU built from the sandbox template; compare reports the CloudTrail guardrail and the security team's audit read LOST. joiner-mover-leaver: group-based offboarding and the direct permission set it cannot see; a trap, not a delay. Writing it, writ found a second bug in the first draft of the safe plan (approve, leave, provision) and the README keeps it. Each failing property names a (show …) query, and each .rules file prints the privilege path. Cross-check 31 -> 41 properties (never: 3 -> 7); 257 checks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A large expense needs the manager's and finance's approval. The shortcut pays when both slots are filled; Bob is manager and finance's deputy, so four allowed steps pay on one person's say-so. Amounts are bands, not numbers. compare reports never-on-one-person LOST while the law it breaks reads preserved (laws compare by declaration); the README says so. In the rules, independence is a join: a rules guard cannot compare a path with a path, though the claims language can. Also documented: in the safe process the only way to undo a signature is to reject, cancel, or change the bank account. Cross-check 41 -> 45 properties (43 compared, 2 fair skipped); 270 checks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…hat leaks Policy v1 allows file reads outright and makes the shell ask; v2 adds a web-fetch allowed outright. compare: no-unapproved-exfiltration LOST in three moves — switch-to-auto, read-secret-with-file-read, send-secret-with-web-fetch — none of them human; the verdict names t = web-fetch. The loop, run against the unedited claims: the honest fix (web-fetch asks) holds everything but stays exit 1 until the human acknowledges its new approval path; the cheat (delete the `out` arrow) turns the safety property n/a and `writ check` EXITS 0 — compare against v1 refuses it. Tested as is. Cross-check 45 -> 49 properties (47 compared); 289 checks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Three instances rolled r1 -> r2 behind a health gate, then a one-way migration. The safe plan fails can-roll-back: the runbook done right, eight steps, ends where r1 is unreachable for good; ct.rules one-way names `migrate` and nothing else. The shortcut drops the health gate and goes dark in four steps. Writing it, writ found a race in the first draft: finish the rollout, decide to roll back, and the migration (guarded on the instances only) runs anyway; the rollback then starts r1 on v2. migrate now also requires target r2. Cross-check 49 -> 52 properties (50 compared); 301 checks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
One order: authorize, capture over a wire that loses replies, settle, ship, refund, cancel. Without a key, a lost reply and a retry charge twice in six steps; derive double-charged shows the order looking normal in every stage. The shortcut also charges for a cancelled order: the void overtakes the capture, finds nothing, and the capture lands after it. Writing it, writ failed the first draft of the SAFE file, key and all: cancel was allowed whenever the shop had not captured, so a capture still on the wire landed after the cancellation. cancel now voids at the processor, under the same key. Cross-check 52 -> 56 properties (54 compared); 314 checks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Four flags and two modes, 64 combinations; the guarded operations reach exactly the 21 the product's rules allow. The shortcut's disable-sso checks authentication but not the shard latch: enable-legacy-auth, shard, disable-sso reaches a forbidden state, and only in that order. --fiber cfg.region shows the EU deployment is safe from it by accident. v2 adds a billing flag whose enable turns tenancy on: compare reports never-unsafe LOST in one move, and check reports the new operation unadmitted. final-phase names exactly the sharded configurations. Cross-check 56 -> 60 properties (58 compared); 329 checks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gotha, calculation, oversight, workflow and access each had 7-12 states, and their findings could be read off the move list or were fixed by the modelling choices. gotha and calculation were also political arguments whose verdicts depended on those choices, not on the search. island stays: its point is that a known paradox shows up as a declared gap. writ control and writ compare --git now run on payments (the idempotency key dropped across two commits loses never-double). The cross-check walks 18 scenarios and 55 properties, and its live assertions point at payments and deployment. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Removes
gotha/,calculation/(andlibraries/economy.lib.writ),oversight/,workflow/andaccess/. Each had 7–12 states, and the finding could be read off the move list or was decided by the modelling choices rather than the search.island/stays: the known paradox appearing as a declared gap is the point.writ controlandwrit compare --gitnow run onpayments. Dropping the idempotency key across two commits losesnever-double.liveassertions now citepaymentsanddeployment../run-tests.sh: 265 passed, 0 failed.Stacking note: this branch sits on
config-space(#9), because the rewired tests usepayments. The base ismainon purpose, so this PR shows #4–#9's commits until they merge and then shrinks to one commit. Merge it after #9.🤖 Generated with Claude Code