Case · AI agents and the controls around them · Public artifacts and one private record

What a mediation boundary establishes, and what it does not

Authorisation layers in front of tool-using agents: a Cedar-mediated tool server, a fault-injected safeguards pipeline, a permit-bound executor, and Microsoft's Agent Framework with its enforcement bundle.

The system said: Limited to 4 KB. 66 tests passed. Replay: VERIFIED. 1,026 actions prevented.
The evidence showed: A 100 KB write executed under the 4 KB cap; all 1,026 prevented actions had run. Mediation held. Binding and position are separate properties with separate evidence.

§ 1

The claim tested

If every action passes the authorisation check, the actions that ran were the ones authorised, and a record of prevention is a record of what did not happen.

§ 2

What Omega did

Wrote the executed effect to a place the agent and its policy layer do not control: the bytes on disk, a second-writer log, the environment's own ledger, side effects observed out of process.
Varied one thing at a time: the position of a control (in the path or beside it), the strength of a forged permit, the presence of an enforcement bundle on a delegated child agent.
Where the claim was about every reachable state or every interleaving, proved it in Lean 4 rather than testing it, and audited the proofs for axioms.
Filed what was found on the vendor framework with its maintainers as a request for a signal, not as a vulnerability.

§ 3

What was found

An agent limited to 4 KB wrote 100 KB while 66 of 66 tests passed and an independent replay verifier said VERIFIED. Mediation held; the binding between the authorised operation and the executed one did not.
A monitor beside the execution path recorded 1,026 actions as prevented. All 1,026 had executed. The same evaluator and policy placed in series recorded 6 of 9,880.
An executor that passed 24 of 24 recorded tests accepted a permit that had never been issued, because it checked that the permit was well-formed and never that it existed.
In Microsoft's Agent Framework, the documented enforcing configuration behaved correctly: every side effect observed out of process had a causally preceding permit for exactly that operation. Two documented configuration requirements produce no signal when violated. A maintainer replied that guarding a delegated agent is the agent author's responsibility and that they do not expect to change this.
A spending cap holds in every reachable state and a capability bound holds over every interleaving, each machine-checked in Lean 4; the capability bound carries 29 audited theorems and no axioms.

§ 4

Verdict

CONTRADICTED: Authorisation checks passed, so the executed operation was the authorised one. In two constructed systems. In the third-party framework, under its documented configuration, it held.
CONTRADICTED: A monitor's record of preventions is a record of what did not happen. Position decides it: in series, 6 of 9,880; beside the path, 1,026 of 1,026 executed.
SUPPORTED: The documented enforcing configuration mediates every out-of-process side effect. For the configurations tested. Misconfiguration produces no signal, and upstream regards that as the integrator's responsibility.
SUPPORTED: The bound holds in every reachable state. Kernel-checked over the model as stated; the model's fidelity to a deployment is the trusted base.

§ 5

What this does not establish

The constructed systems were built for the study; they say what is buildable, not what deployed agents do. The proofs cover terminal-observation safety inside a stated model, with no liveness and no machine-checked link to code. The framework result is the public issue text only. No agent product is certified by any of this.

§ 6

Upstream

Microsoft Agent Framework (Python) with its agent-hooks enforcement bundle OPEN ISSUE issueWhether the documented enforcing configuration mediates every side effect observed out of process, and what signal exists when a delegated child agent or a later-placed middleware sits outside it. Issue #8050, 4 September 2026. Open issue. A maintainer replied on 4 September 2026 that guarding a delegated agent is the agent author's responsibility and that they do not expect to change this; no later maintainer response as of 20 September 2026.

Released means the fix is in a tagged release. Merged means it is on the default branch but not verified in a tagged release. Open pull request means an Omega-authored change awaits upstream action. Open issue means a report remains open without a merged fix. Maintainer acceptance is review of one change, not endorsement of Omega.

§ 7

The records

Every field of each finding this case rests on, as it appears on the ledger.

OBSERVED authorized-limit-and-executed-write-disagreedauthorise · faithfulness An agent was limited to 4 KB. It wrote 100 KB. Every test passed, an independent replay verifier said VERIFIED, and a checked invariant held.

Claim: A write of 100,000 bytes executed under a policy that capped writes at 4,096 bytes, while 66 of 66 tests passed, an independent replay verifier returned VERIFIED, and a checked complete-mediation invariant held.

Status: OBSERVED Witnessed in one instance. No claim about how often.

Question: Authorised is not executed

Subject: A Cedar-mediated MCP tool server built for the study (authored). built for the study

Frame: One server, six tools, 25 adversarial scenarios; the write cap is a policy constant.

Method: Every decision is written to a hash-chained ledger that an independently written replay verifier reads back; four properties (mediation, binding, policy adequacy, effect verification) are reported separately.

Oracle: The bytes actually written to the fixture, read back independently of the executor.

Negative control: Present The repair is re-attacked with a falsification sweep; the version-one audit is preserved so the failing state can be re-run.

Denominator: 66 of 66 tests in version one; one write of 100,000 bytes against a 4,096-byte cap.

Limitation: One defect in one server built for this study, not a measurement of deployed systems and not a claim about how often authorization layers and executors diverge. Mediation held throughout; what failed was the binding between the authorized operation and the executed one. Policy adequacy is separately not established, and two counterexamples covering it are retained unfixed.

Source: repowazdogz-droid/mcp-authority-boundary @ 03854ddc

Reproduce: npm install && ./run.sh

Independent reproduction: None known.

This finding on its own page

MEASURED monitoring-arm-recorded-preventions-that-executedobserve · observation boundary A dashboard reported 1,026 actions prevented. All 1,026 had already executed.

Claim: Over 10,000 injected events, a monitoring arm recorded 1,026 actions as prevented and all 1,026 executed; an in-series arm consuming the same events, evaluator and policy recorded 6 of 9,880.

Status: MEASURED Empirical, with a stated sample.

Question: Recorded is not observed

Subject: A synthetic, deterministic fault-injected pipeline on Redis Streams (authored). built for the study

Frame: 10,000 injected events, fail-closed policy; both arms consume identical events, evaluator and policy and differ only in position.

Method: Two arms, one on the execution path and one observing beside it; a second axis varies single-writer versus two-writer telemetry.

Oracle: The executed-action log, written by a second writer that the monitor does not control.

Negative control: Present Nine negative controls in the repository; CI deletes the committed results and regenerates them.

Denominator: 1,026 recorded as prevented, 1,026 executed; in-series arm 6 of 9,880; intervention recall 0 of 818 versus 697 of 818.

Limitation: A property of one synthetic, deterministic testbed under injected faults, not a measurement of any deployed safeguards product and not a rate that transfers outside this harness. The agent environment is deliberately trivial so that what is measured is the pipeline rather than model behaviour.

Source: repowazdogz-droid/safeguards-control-plane @ 08e52549

Reproduce: ./demo.sh && make experiments

Independent reproduction: None known.

This finding on its own page

OBSERVED n-1-permit-membershipexecute · coverage illusion A program passed all 24 of its recorded tests and still accepted a permission record that had never been issued.

Claim: A start permit assembled entirely from public registry facts, with its reference number derived by the authorizer's own function and committed to no ledger, was accepted by the bounded executor and the registry-named transform was applied; the target's bytes changed.

Status: OBSERVED Witnessed in one instance. No claim about how often.

Question: Authorised is not executed

Subject: The frozen STARTAUTH-01 executor, attacked from outside; the minimal public reproduction re-creates the defect in a small program. built for the study

Frame: One executor, one registry-named transform, one target file; forgery built from public registry facts.

Method: Three forgeries of increasing strength handed to the executor; bytes hashed before and after.

Oracle: The target bytes, hashed before and after each case.

Negative control: Present S16 and S17, the two weaker forgeries, were refused. Their refusals are what make the third result legible.

Denominator: 24 of 24 recorded cases matched their expectation; one of them (S18) expected the failure.

Limitation: One defect in one program built for this study. Not a measurement of deployed systems, and no claim about how often authorisation records are treated as evidence of authorisation. Not a break-in: producing the forgery requires the ability to run code as the same user, and such an actor can edit the target directly without any record. The minimal fix establishes that a membership check closes this specific defect; it does not establish at-most-once execution, atomic consumption, or independent measurement of the effect.

Source: repowazdogz-droid/omega-n1-permit-membership @ efba311

Reproduce: git clone https://github.com/repowazdogz-droid/omega-n1-permit-membership && cd omega-n1-permit-membership && python3 reproduce.py

Independent reproduction: None known.

This finding on its own page

PROVEN budget-bound-for-all-reachable-statesauthorise A spending cap was proved to hold in every state the system can reach, not just the ones anyone tested.

Claim: Total spend never exceeds the cap in any reachable state of the escrow protocol, proved in Lean for any finite set of replicas and any non-negative amounts.

Status: PROVEN Follows from stated premises inside a named frame.

Question: Individually compliant is not collectively safe

Subject: A Lean 4 model of the escrow protocol (model). built for the study

Frame: Any finite set of replicas, any non-negative amounts; crash is global in the Lean model.

Method: Induction over reachable states with the budget bound as the invariant; a TLA+ model and a Python fault harness exercise what the proof does not.

Oracle: The Lean 4 kernel (v4.32.0), axioms propext and Quot.sound only.

Negative control: Present Four proved negative controls: remove a guard and the theorem must fail.

Limitation: The bound, not conservation. No liveness, availability, or Byzantine model; crash is global in the Lean model, and per-replica crash is only exercised in the bounded checks. The proof holds relative to the transition system being a faithful abstraction of the protocol, which is argued, not machine-checked.

Source: repowazdogz-droid/escrow-budget @ 9c199db4

Reproduce: make clean && make check

Independent reproduction: None known.

This finding on its own page

PROVEN concurrent-capability-bound-over-interleavingsauthorise A limit on what an agent may do was proved to hold no matter how concurrent operations interleave.

Claim: A capability meter never exceeds its cap over every concurrent interleaving of charge operations, proved in Iris concurrent separation logic for any cap and any finite list of operations.

Status: PROVEN Follows from stated premises inside a named frame.

Question: Individually compliant is not collectively safe

Subject: A Rocq/Iris model of a concurrent capability meter (model). built for the study

Frame: Any cap, any finite list of charge operations, every interleaving; terminal-observation safety only.

Method: Adequacy over every reachable configuration in Iris concurrent separation logic.

Oracle: The Rocq kernel; Print Assumptions committed and diffed in CI.

Negative control: Present Floor E: an explicit counterexample showing per-key safety does not certify a tighter cross-key aggregate bound.

Limitation: It is terminal-observation safety, the value the driver reads is within the cap, not an all-intermediate-state invariant, and it carries no liveness or wait-freedom. The kernel check was not re-run in this pass; axiom-freedom rests on the committed assumptions audit plus a live search finding no admitted goals.

Source: repowazdogz-droid/capctl-iris @ 5e9284a0

Reproduce: eval $(opam env --switch=capctl-iris) && make verify

Independent reproduction: None known.

This finding on its own page

All cases Bring us a problem