demo: multi-agent verification scenario (agents + independent synthesis)#20
Merged
Conversation
…ervisor verifies) Two agents share one repo at once, each on its own branch. verify.sh (the deterministic supervisor) launches agent-a and agent-b CONCURRENTLY, each in its own guarded session running agent-run.sh; each agent does real work, pushes its own branch, tries to interfere with the other, and leaves a machine-recomputable evidence bundle (every command's raw stdout/stderr/exit-code + a state snapshot). Per the adversarial design review: an agent's own PASS is not proof — the supervisor RE-DERIVES the truth from git/home/audit state (never the agent's narrative) and checks nine invariants: distinct worktrees on bound branches, git-is-the-shim in both sessions, both branches on the shared origin, per-agent provenance (not mixed), isolated working trees, the shared source repo untouched, one integrity key with both signed bindings, every guarded step behaving (own push ok; cross-agent checkout/force-push/delete all DENIED), and each agent's self-verdict consistent with the re-derived state. Invariant 8 reads the real exit codes, so it FAILS if a guard doesn't fire — it is designed to catch a regression of exactly the cross-agent force-push clobber (PR #19) whose gap this scenario's design first surfaced. Verified end-to-end (9/9 invariants held with the installed 0.2.2 + PR #19). Throwaway world in a temp dir; only remote is a local bare repo. shellcheck clean (SC2015 excluded: pass/bad are non-failing printf helpers). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…se forged-artifact hole) fugu review REJECTED: the synthesis still trusted agent-written artifacts for the canonical-checkout invariant. It only checked the shared project repo, never the stand-in real checkout, and took the agent's own rc/verdict files as the source of truth — so an agent could move the canonical checkout's HEAD, write 10.rc=1 + verdict=PASS, and the synthesis reported success (fugu reproduced it). Rewrite the synthesis to RE-DERIVE every invariant from independent state: - worktrees come from the shim-written, HMAC-signed bindings (not the agent's evidence.env); each worktree's current branch is read with real git (catches a cross-branch checkout that drifted HEAD). - cross-agent push/delete is caught by the origin state itself: both branches present, distinct, each trailered to its OWN agent. - NEW: the stand-in real checkout's HEAD must equal its pre-run value — this independently catches an agent touching your checkout regardless of what it reported (the exact hole). - the agent's rc/verdict becomes a CONSISTENCY cross-check only: it can flag a self-report that disagrees, but can never turn a real violation into a pass. Verified: normal run VERIFIED (11 invariants, re-derived); and fugu's forge attack — tamper the canonical HEAD + fake agent-a's 10.rc=1/verdict=PASS — is now caught by the independent canonical invariant. shellcheck: verify.sh fully clean; agent-run.sh clean except an intentional single-quoted sh -c (SC2016). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…writable HOME fugu review REJECTED again (deeper): the synthesis called binding.json authoritative but never verified its HMAC signature — I5 only checked that .sig FILES exist. A same-uid agent with $AGENTIC_GIT_HOME can rewrite its binding.json to point at a fake clean repo (sig stale but present), and the synthesis accepted the fake worktree. fugu reproduced it. Root cause: HOME is agent-writable at same-uid (the agent can even read the HMAC key and re-sign), so NO home-derived state is trustworthy against a malicious agent — the seatbelt-not-cage limit. Fix: the supervisor now derives the agents' worktrees from the SHARED PROJECT's own `git worktree list` (the supervisor owns the project repo; an agent can't redirect it by editing HOME). Dropped the cosmetic file-leak check (an agent can create any file in its own worktree — no signal). All the load-bearing invariants already key off supervisor-owned state (bare origin branches + provenance, the stand-in checkout's HEAD, the project's HEAD). README now states the honest boundary explicitly: this verifies the guards for agents going THROUGH the shim (the threat model); a malicious same-uid agent that forges its HOME state or bypasses the shim via /usr/bin/git is out of scope — which is exactly why the supervisor keys off repos it owns, not the agent's home. Verified: normal run VERIFIED; the binding-forgery no longer redirects the supervisor (it reads the project's worktree list → the real worktree). verify.sh shellcheck clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… stale claims) fugu review REJECTED (documentation): after moving the load-bearing checks to supervisor-owned state, the README still advertised invariants the code no longer has — a nine-item list including "working trees isolated (file-leak)" (dropped as cosmetic) and "invariant 8 reads exit codes to prove guarded steps behaved" (exit codes are now only the non-authoritative consistency cross-check). A reader was told the scenario proves properties it no longer checks — the opposite of the honest boundary this scenario is about. Rewrite the invariant list and the "why it's a real test" section to match the actual supervisor-owned checks: the shared project's own worktree list, origin branches + per-agent provenance (this is what catches a clobber), the shared repo's and the stand-in checkout's HEADs unchanged, one non-split-brain key, per-agent audit attribution, plus the agents' self-report as a consistency cross-check only. Also fix the intro's "re-derives from git/home/audit" to "state it owns … never the agent's home". Docs only; verify.sh unchanged (fugu confirmed the code-side forge fixes at 94589cc). Co-Authored-By: Claude Opus 4.8 <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 join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
What
Two agents share one repo at once, each on its own branch — and the scenario checks the multi-agent invariants actually hold.
verify.shlaunches agent-a and agent-b concurrently, each in its own guarded session runningagent-run.sh. Each agent does real work, pushes its own branch, tries to interfere with the other, and leaves a machine-recomputable evidence bundle.Design point (adversarial review): an agent's own PASS is not proof. The supervisor re-derives the truth from git/home/audit state (never the agent's narrative) and checks nine invariants — distinct worktrees on bound branches · git-is-the-shim in both sessions · both branches on the shared origin · per-agent provenance (not mixed) · isolated working trees · shared source repo untouched · one key + both signed bindings · every guarded step behaving (own push ok; cross-agent checkout/force-push/delete all DENIED) · each self-verdict consistent with state.
Why it's a real test
Invariant 8 reads the actual exit codes, so it FAILS if a guard doesn't fire — it is designed to catch a regression of exactly the cross-agent force-push clobber (PR #19) whose gap this scenario's design first surfaced.
Verification
./demo/multi-agent/verify.sh→ 9/9 invariants held with the installed 0.2.2 + PR feat(push): a bound agent may push only its own branch (close cross-agent clobber) #19.shellcheckclean (SC2015 excluded —pass/badare non-failing printf helpers).No
src/changes.🤖 Generated with Claude Code