Validation
Example Validation Matrix
This page summarizes the demo's example validation matrix: self-constructed workflow examples checked by a dependency-free bounded reference checker (the Replay Verifier engine), with an optional Z3 sanity cross-check on supported examples.
What this page is — and is not
What it is
- self-constructed demo examples and customer-style dry runs
- reference-checker regression evidence on those examples
- optional Z3 sanity cross-check on supported examples
- reconstructable trace and retest shape evidence
What it is not
- independent third-party benchmark validation
- third-party repeatability of the demo
- production-security validation
- a global agent-safety claim
What Has Been Exercised
Reference-Checker Regression
Bounded reference-checker tests pass on the included self-constructed workflow examples.
Z3 Sanity Cross-Check
The optional Z3 backend agrees with the bounded reference checker on supported examples in the local development environment. This is an implementation-QA sanity cross-check, not independent real-world validation.
Customer-Style Dry Runs
Customer-style dry runs were exercised across support, refund, permission, and data-export workflow shapes without verifier source-code changes.
Trace and Retest Shape
Unsafe cases return reconstructable traces. Guarded variants return SAFE_WITHIN_BOUND under the supplied model and bound.
Demo Exercise Matrix
This in-page table mixes canonical self-constructed demo examples and customer-style dry-run shapes. The downloadable matrix at docs/repeatability_validation_matrix.md covers the customer-style dry runs; the canonical demo example artifacts (including the larger vendor-payment pair) are documented separately in docs/validation_run_evidence.md.
| Workflow shape | Failure shape | Unsafe Result | First Bad Step | Guarded Variant Result | Z3 Sanity Cross-Check |
|---|---|---|---|---|---|
| Support reply (dry run) | External reply after customer account data access before manager approval. | UNSAFE | 4 | SAFE_WITHIN_BOUND | Agreed |
| Refund approval (dry run) | Refund issued before manager approval. | UNSAFE | 4 | SAFE_WITHIN_BOUND | Agreed |
| Permission escalation (dry run) | Elevated access granted before administrator authorization. | UNSAFE | 4 | SAFE_WITHIN_BOUND | Agreed |
| Data export (dry run) | Sensitive data exported before export authorization. | UNSAFE | 3 | SAFE_WITHIN_BOUND | Agreed |
| Email exfiltration (canonical) | Customer data emailed externally without approval. | UNSAFE | 3 | SAFE_WITHIN_BOUND | Agreed |
| Delete confirmation (canonical) | File deletion before confirmation. | UNSAFE | 2 | SAFE_WITHIN_BOUND | Agreed |
"Z3 Sanity Cross-Check: Agreed" means the optional Z3 backend produced the same status as the reference checker on that example. Agreement is necessary and useful for implementation QA, but it is not independent real-world validation.
Why This Matters
The same audit pattern was applied across multiple self-constructed workflow shapes without changing verifier source code. That supports the service workflow — intake, model, check, trace, remediate, retest — not unrestricted system safety.
Limits of This Evidence
This is example-level evidence on self-constructed workflows. It does not establish independent benchmark validation, third-party repeatability, production-security validation, or global agent-safety. Results are bounded to the supplied workflow model and configured search depth.