[Feature] Stateful trajectory assertion for forbidden world states

[thegobi]

Problem statement

The harness can currently reject a denied tool call or an external recipient, but a trajectory can still reach a prohibited outcome through calls that are individually permitted.

For example, an agent may read confidential records, transform them, create an archive, upload it, and send a link. No single call needs to be forbidden; the security failure exists in the resulting world state and in the provenance connecting the steps. The same composition problem appears with split payments, gradual permission changes, or staged publication.

A per-trace assertion therefore needs a deterministic way to evaluate cumulative effects and provenance, not only isolated tool names or arguments.

Proposed solution

Add a narrowly scoped, vendor-neutral assertion family for a candidate name such as forbidden_state_not_reached.

The first version could stay intentionally small:

1. A scenario declares a deterministic state model and one or more forbidden predicates.
2. Recorded trace events carry normalized effects and provenance references.
3. The assertion folds those effects in order, evaluates the predicate after every transition, and fails at the first forbidden state.
4. Failure evidence reports the transition index, predicate ID, and redacted provenance chain.
5. A paired control scenario demonstrates that the assertion does not block an equivalent legitimate workflow.

This does not require an LLM judge, a policy language, credential brokerage, or a general simulator. A minimal implementation could begin with one concrete outbound-data composition scenario and a small deterministic reducer.

The broader defensive architecture that motivated the proposal keeps service credentials outside the agent, issues narrow expiring one-use capabilities only after candidate-state evaluation, and records decision/execution provenance in an append-only evidence chain. That architecture is context for the assertion, not a requested dependency of the harness.

Alternatives considered

• Deny the final tool call. This misses allowed recipients, allowed storage destinations, split transactions, and other cases whose risk depends on cumulative provenance.
• Add more tool/argument rules. Useful, but it still treats each call in isolation and can recreate a large brittle allowlist.
• Use an LLM as judge. Broader, but conflicts with the harness preference for deterministic assertions and complicates reproducibility.
• Keep this outside the harness. Reasonable if normalized state transitions are judged too broad; in that case, a documented adapter contract for an external stateful assertion would still be useful.

Scope

In scope for an initial design discussion:

• one deterministic multi-step scenario;
• one paired legitimate control;
• a minimal normalized-effect/provenance shape;
• one assertion that fails when a declared predicate becomes true;
• tests showing both attack detection and control completion.

Out of scope:

• claiming complete world-state models or production security;
• model or vendor rankings;
• adaptive attack-rate estimates;
• generic policy engines or LLM-as-judge;
• requiring the CCG or ITHZ implementation in the harness.

Reproducible pilot offered as design evidence

The public pilot that exposed this gap used exactly one OpenClaw version, one low-cost model, four author-built attack/control pairs, known author-built predicates, deterministic synthetic services, and one run per condition (24 runs total). Observed forbidden-state counts were direct forwarding 4/4, stateless per-call policy 3/4, and stateful candidate-world authorization 0/4; all three conditions completed 4/4 paired legitimate controls.

This is author-designed pilot evidence, not a benchmark, independent replication, real-world attack-success estimate, proof of predicate completeness, production certification, or OWASP endorsement.

• Frozen evidence and verifier: https://ithz.dev/docs/releases/
• Public repository and release: https://github.com/thegobi/ccg-ithz-trajectory-pilot
• Protocol: https://ithz.dev/docs/CCG_REAL_AGENT_PROTOCOL_EN.md

The most useful early criticism would be whether this can remain a small deterministic regression assertion, and which single scenario would best expose the state-model boundary without turning the harness into a general evaluation platform.

AI-assistance disclosure

This issue text was drafted with OpenAI Codex under the author's direction. The human author reviewed the proposal, owns the linked work, and remains responsible for the claims and any follow-up contribution.

[abhinav-phi]

Hi! I'd like to work on this feature.
Plan: I'll implement the stateful trajectory assertion for forbidden actions — track agent state across steps, evaluate forbidden-action rules against the full trajectory, and add unit tests plus documentation.
Could you please assign this to me? Thanks!

/assign
take

[thegobi]

Thanks, Abhinav — I’d be very happy to see you work on this. I’m the issue proposer rather than a repository maintainer, so I can’t assign it myself. Please wait for maintainer confirmation before investing in a large implementation. To keep the first version reviewable, I suggest starting with one deterministic reducer, one attack/control pair, normalized effects and provenance, and failure evidence containing the transition index, predicate ID, and redacted provenance chain. No LLM judge or CCG/ITHZ dependency should be required. A short design sketch before the full PR would be especially useful. I’m happy to clarify the experiment, predicates, and evidence format.

[ossumpossum]

On the scope question you raised: yes, this can and should stay a small deterministic regression assertion. For "which single scenario best exposes the state-model boundary," the read-transform-archive-upload-send outbound-composition case you sketched is the right first one, since the failure lives entirely in the cumulative state and provenance and none of the individual calls are forbidden.

Two notes, both about how far the assertion's guarantee reaches:

1. Predicate order-sensitivity. Worth stating for the first scenario whether the forbidden predicate is order-sensitive or commutative over effects. If it is commutative (the forbidden state is reached regardless of interleaving), fold order does not matter and this is a non-issue. If it is order-sensitive, then the recorded event order is the contract the reducer depends on, which the transition-index design already implies, so the recorder should stamp a monotonic per-trace sequence at record time rather than lean on arrival time. That keeps the same scenario stable across recordings, not only across re-runs of one fixed trace.

2. State-model coverage as a stated precondition. You have already scoped out complete world-state models, which is the right call for a first version. The one thing worth writing into the assertion's docs is that its guarantee is bounded by the state model's coverage of effect channels: an outcome reached through an unmodeled channel will not appear in the fold, and the assertion passes. That is a documentation precondition, not a dependency, and it keeps the assertion from being read as stronger than the effects it sees. In a live setting the evidence-chain integrity you describe as context is what backs that precondition, though for the authored fixtures here the effect stream is trusted by construction.

[thegobi]

Thanks — I agree with both points.
For the initial scenario, I would make the forbidden predicate order-sensitive and treat the recorded monotonic per-trace sequence as part of the assertion contract.
I also agree that state-model coverage must be an explicit precondition: the assertion can only detect forbidden outcomes represented by the modeled effect channels. It should not be presented as a complete world-state guarantee.
The read → transform → archive → upload → send scenario is a good first regression case because no individual operation is forbidden; the failure emerges only from cumulative state and provenance.
I’ll review PR #174 with these boundaries in mind. Thank you for sharpening the scope.

[abhinav-phi]

Thanks @ossumpossum and @thegobi — both points are incorporated in PR #174 (commits 6dd8dab and 21c3828):

Order-sensitive predicates + monotonic sequence contract. The bundled scenario's predicate is now order-sensitive: the external-upload transition carries a requires guard on confidential_data_loaded, so an upload that precedes the read never increments the exfiltration counter, while read-then-upload does. Effect events may stamp a monotonic integer sequence at record time; when every effect event stamps one, the stamped order is the authoritative fold order, so the same recording folds to the same verdict regardless of how its JSON array was re-serialized. No stamps falls back to arrival order for backwards compatibility; mixed, duplicate, or non-integer stamps surface as an error result, since the recorded order is then unreliable evidence rather than a pass/fail verdict. The bundled fixtures stamp sequence, and tests cover sorting, reordering stability, both guard orders, and every rejection path.

Coverage precondition. The assertion doc now states explicitly that the guarantee is bounded by the state model's coverage of effect channels: an outcome reached through an unmodeled channel never appears in the fold and the assertion passes. A pass means "no forbidden state among the modeled effects", not "in the world". For authored fixtures the effect stream is trusted by construction; in live settings, evidence-chain integrity is what backs the precondition — documented as a precondition, not a dependency.

Docs updated: docs/assertions/forbidden-state-not-reached.md (new "Order sensitivity and the sequence contract" and "Coverage precondition" sections), docs/trace-format.md (sequence field), scenario-spec, README, and the CHANGELOG entry.