Refund Guardrails

What This Example Proves

Refund guardrails is the canonical business-rule enforcement proof story for JacqOS. Two AI agents — customer support and finance — coordinate through a shared derived model to process refunds. The ontology enforces safety invariants that prevent unsafe payouts regardless of what either agent proposes.

The example proves four things that are hard to get right without a satisfiability boundary:

1. No refund above threshold without approval. High-value refunds require explicit manager authorization before any payout is executed. The requires_approval invariant blocks the intent until the approval observation arrives.
2. No payout after dispute or fraud flag. Once a chargeback or fraud signal arrives, the ticket is risk-blocked and no payout can proceed. The no_payout_after_dispute invariant fires immediately.
3. No duplicate payout. At most one successful payout per ticket, preventing double-refund scenarios even if the finance agent retries.
4. Exactly one terminal state. A ticket cannot be both resolved and rejected, ensuring a clean audit trail.

Who This Is For

Use this example if you are building agent systems where:

• LLM agents make financial commitments that need hard safety boundaries
• Business rules must be enforced regardless of what the model proposes
• Approval workflows need provable gate enforcement, not just prompt guardrails
• Audit trails must trace every payout decision back to specific observations

Proof Surfaces to Inspect

Studio Screenshots

The website/public/proof/refund-guardrails/ directory contains Studio captures of the two key proof moments:

Blocked intent. A payout intent on a disputed ticket rejected by the no_payout_after_dispute invariant. The support agent proposed a refund, but the chargeback observation arrived first — the intent exists but the effect is blocked.

Provenance trace. A complete chain from the ticket-opened observation through refund request, LLM commitment proposal, manager approval, and payout execution — every step traceable.

Fixtures

Four fixture paths exercise different proof surfaces:

Fixture	What it proves
happy-path.jsonl	$49.99 refund under threshold — payout authorized and executed, customer notified
escalation-path.jsonl	$250 refund above threshold — payout authorized after manager approval, executed via bank transfer
contradiction-path.jsonl	$175 refund approved by manager, but charge disputed — no_payout_after_dispute invariant blocks payout; ticket rejected
coverage-path.jsonl	$500 refund with fraud flag, no approval — no_payout_after_dispute fires; requires_approval without approval; ticket rejected

Generated Artifacts

Artifact	Path
Evaluation package	generated/jacqos-v1/jacqos-refund-guardrails.evaluation-package.json
Fact export	generated/jacqos-v1/jacqos-refund-guardrails.default.fact-export.json
Graph bundle	generated/graphs/jacqos-refund-guardrails.graph-bundle.json
Benchmark report	generated/verification/jacqos-refund-guardrails.benchmark-report.json
Composition analysis	generated/verification/composition-analysis-sha256-*.json
Verification suite	generated/verification/jacqos-refund-guardrails.json
Counterexamples	generated/verification/counterexamples/

Repo Artifacts

The full example source lives in examples/jacqos-refund-guardrails/:

• Ontology — ontology/schema.dh, ontology/rules.dh, ontology/intents.dh
• Mappings — mappings/inbound.rhai, mappings/providers.rhai
• Fixtures — fixtures/*.jsonl (four paths covering happy, escalation, contradiction, coverage)

Quick Start

See the example README for setup commands and directory layout:

jacqos dev
jacqos replay fixtures/happy-path.jsonl
jacqos verify
jacqos studio

Next Steps

• Observation-First Model — how the pipeline works
• Golden Fixtures — fixture verification in detail
• Invariant Review — how invariants replace code review
• Visual Provenance — tracing facts back to observations in Studio