Bounded Replay-Risk Audit Demo
Find dangerous workflow paths before deployment.
A pre-deployment workflow check for AI-agent and SaaS workflows: does a reachable action ordering bypass an approval, confirmation, or escalation gate within the supplied model and bound?
Example: a wire can be sent without verification
In the vendor-payment workflow, the model includes vendor verification, compliance review, and manager approval actions. The unsafe version still allows send_wire after wire_prepared without requiring those gates. The Replay Verifier finds the reachable path:
read_invoice → access_vendor_record → access_payment_system → prepare_wire → send_wire
The guarded variant requires vendor_verified, compliance_review_passed, and manager_approved before send_wire, and retests SAFE_WITHIN_BOUND under the supplied model and bound.
The point is not that the action send_wire is individually mysterious; the risk is that reviewers may assume earlier preparation implies verification when the model does not actually enforce it.
Approval gates only protect against composed misuse if the workflow definition actually forces the agent through them.
About the Audit
A bounded replay-risk audit checks whether a scoped workflow can reach a prohibited outcome before the required approval, confirmation, or escalation gate occurs. It is a pre-deployment workflow check that is useful when a team can describe a workflow as actions, preconditions, effects, and a bad outcome to avoid.
Find Bad Paths
Locate reachable bad paths before deployment.
Locate the Guardrail
Identify the missing approval, confirmation, or escalation precondition.
Retest the Fix
Retest the guarded variant under the same bound.
What It Does
Scoped Workflow Model
Models a scoped workflow as Boolean states and actions. The model is explicit about what is inside the audit and what is outside it.
Bounded Search
Searches for reachable bad action sequences within a configured bound. The result is tied to that supplied model and depth.
UNSAFE Trace
Returns UNSAFE with a reconstructable trace if a violation is reachable within the model and bound.
Guarded Result
Returns SAFE_WITHIN_BOUND if no violation is found within the supplied model and bound.
What You Get
The audit produces a Bounded Replay Verification Report packaging the items below.
Exact Bad-Path Trace
The report identifies the action sequence that reaches the prohibited state.
Missing Guardrail Diagnosis
The audit highlights where an approval, confirmation, or escalation precondition is missing.
Remediation Note
The package records the candidate guardrail and the retest requirement.
Safe-Variant Retest
A guarded variant can be checked with the same verifier semantics.
Explicit Assumptions
Each dry run documents what the model assumes, excludes, and can support.
Current Demo Status
- Dependency-free bounded reference checker (the Replay Verifier engine).
- Optional Z3 sanity cross-check against the reference checker for supported examples.
- Self-constructed example workflows across multiple failure shapes.
- Customer-style dry runs completed without verifier source-code changes.
Why This Matters for AI Agent Tool-Use Safety
LLM-driven agents make tool-use decisions by reasoning over their available actions. When an agent is given a bag of tools, it can sometimes find an action ordering that satisfies the immediate request while bypassing intended guardrails — even when no individual tool call looks like misuse. Approval gates only protect against composed misuse if the workflow definition actually forces the agent through them.
This audit gives builders a way to model the intended workflow as a small Boolean state machine and ask: is there any reachable action ordering that reaches a forbidden composed state within a given depth? When the answer is UNSAFE, the audit returns the exact step sequence as a reconstructable counterexample, identifies the step where the bad state first appears, and supports a guarded-variant retest after the missing precondition is added.
Failure shapes covered by the demo include workflow approval bypass, confirmation bypass, permission escalation, sensitive data export before authorization, and composed action ordering across tool-use steps.
Where it fits
Pre-deployment workflow review during agent design and review. Complementary to runtime guardrails like prompt-safety filters, tool permission scopes, and per-call approval UIs — it catches a different class of failure (composed action ordering) before deployment, in a small artifact a team can version-control alongside the agent definition.
Where it does not fit
This is not a probabilistic LLM behavior model, not a runtime monitor, not an IAM/cloud graph analyzer, and not a replacement for security review. It does not reason about prompt injection, tool output content, or whether the agent will choose any particular path at runtime — only whether the path exists in the workflow definition.
Review Next
Review the validation matrix or start with the audit package.