Examples

Examples

Self-constructed demo examples. Each one identifies the bad path, the missing guardrail, the candidate fix, and the retest result under the supplied model and bound.

Vendor Payment Without Verification

Larger workflow: 9 state variables, 8 actions, bound 8. The bad path is not obvious by reading the JSON. This example illustrates composed action ordering: every individual tool call looks permitted, but a reachable ordering reaches the forbidden composed state.

Bad Path

Read invoice → access vendor record → access payment system → prepare wire → send wire

Technical Trace

read_invoice → access_vendor_record → access_payment_system → prepare_wire → send_wire

Why It's Easy to Miss

The workflow has separate actions for access_vendor_record (look up the vendor) and verify_vendor (perform verification). A reviewer reading send_wire's preconditions sees only wire_prepared: true and may assume that path implies vendor verification. The forbidden condition checks vendor_verified directly, so the workflow reaches the bad state at step 5 even though vendor verification, manager approval, and compliance review are all available actions. 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.

Missing Guardrail

send_wire did not require vendor_verified, compliance_review_passed, or manager_approved.

Fix

Require vendor_verified, compliance_review_passed, and manager_approved before send_wire.

Retest

SAFE_WITHIN_BOUND under supplied model and bound. The optional Z3 sanity cross-check (brute-force vs. Z3) returned status_match: True on both variants. This is implementation-QA agreement on a self-constructed example, not independent real-world validation.

Artifacts

Support Agent External Reply

Bad Path

Read ticket → access account data → draft reply → send externally

Technical Trace

read_ticket → access_customer_account_data → draft_reply → send_reply_external

Missing Guardrail

send_reply_external did not require manager_approval_received.

Fix

Require manager_approval_received before send_reply_external.

Retest

SAFE_WITHIN_BOUND under supplied model and bound.

Refund Without Manager Approval

Bad Path

Read refund request → access billing record → draft refund → issue refund

Technical Trace

read_refund_request → access_customer_billing_record → draft_refund → issue_refund

Missing Guardrail

issue_refund did not require manager_approval_received.

Fix

Require manager_approval_received before issue_refund.

Retest

SAFE_WITHIN_BOUND under supplied model and bound.

Destructive Delete Without Confirmation

Bad Path

Select file → delete file

Technical Trace

select_file → delete_file

Missing Guardrail

delete_file did not require confirmation_received.

Fix

Require confirmation_received before delete_file.

Retest

SAFE_WITHIN_BOUND under supplied model and bound.

Pattern

The audit shows the exact sequence, the step where the bad state appears, and the guardrail needed to block that path.