# 11 · Assurance Formulas & Boundaries

> What "proven" means, exactly.

## Overview

"Audited", "secured", "verified" are marketing words until they are formulas.
This page defines the exact conjunctions under which Arcana claims assurance,
and the boundary model that limits every claim.

## The three assurance formulas

```text
ActionAssured   ⇔ traceHealth = COMPLETE
                  ∧ unauthorizedExecutions = 0
                  ∧ orphanExecutions = 0

ApprovalAssured ⇔ traceHealth = COMPLETE
                  ∧ replayExecutions = 0
                  ∧ substitutionsAccepted = 0

InfoFlowAssured ⇔ traceHealth = COMPLETE
                  ∧ secretExfiltration = 0
                  ∧ unlabeledConsequential = 0
```

Each requires traceHealth = COMPLETE first: zero violation counts over a
DEGRADED trace prove nothing.

## Two enforcement boundaries

| Boundary | Enforced by | Example |
|---|---|---|
| Logical | The PEP — final authorization decision, calls the protected adapter | Capability check before spawning a shell |
| Physical | OS, sandbox, container, credential broker, network mediator | Sandbox preventing a path around the wrapper |

```text
StrongEffectAssurance =
  LogicalPEPEnforcement ∧ PhysicalBypassResistance ∧ CompleteEvidence
```

All three, or the claim is weak. A TypeScript wrapper is not kernel-enforced
containment; the effect coverage matrix records, per effect path, which
boundary actually holds.

## Epistemic completion contract

```text
user objective
  → acceptance criteria
  → proof obligations
  → evidence sources
  → verifier result
  → completion state
```

No evidence, unmet criterion, or invalid integrity ⇒ **not verified
complete**. Completion is a derived judgment over evidence, never asserted.

## Nonclaims (what is NOT claimed)

- No hostile-host containment claim where only logical enforcement exists.
- No universal external-CLI governance.
- No fleet production claim before live validation levels rise.
- External runtime launch (`arcana launch codex|claude|gemini`) provides
  declaration, supervision, and durable evidence — explicitly **no sandbox
  claim**.

## Conformance summary

46 golden vectors (TS + Rust agree) · TS crypto 100/100 · D-10 hostile matrix
15 fixtures / 0 bypasses · adapter hash vectors 4/4 · external reproduction
(L3) remains the publication gate.

## Related

- Previous: [RunProof — Portable Evidence](/governance/runproof.md)
- Index: [Governance overview](/governance/overview.md)