Skip to content

Architecture

Scope: This document describes the Node CLI shipped by this repository first, then the Seal family assurance lineage. The state machine is TESTED. For the truth about what you installed, read release evidence and the README.

Shipped Node product path

Section titled “Shipped Node product path”
flowchart LR
    claude["Claude Code\n(MCP client)"]
    proxy["Node proxy\nspine/proxy.cjs"]
    state["TESTED state machine\nhandle · freshness · protocol · one-use"]
    wasm["pinned vendored WASM; load-bearing"]
    server["Selected MCP server\nselected tool calls, optionally by argument pattern"]


    claude --> proxy
    proxy --> state
    state --> wasm
    wasm --> server

The shipped Node CLI keeps continuation state in Node and sends only the authorization sub-question through the vendored WASM. A guarded retry follows spine/proxy.cjs → contract/contract.cjs → contract/kernel-authorization.cjs → contract/pinned-kernel.cjs → seal_init → seal_decide. The WASM answer is load-bearing: BLOCK, unreadable output, a hash mismatch, or a Node/kernel disagreement all refuse, with no JavaScript authorization fallback.

Node still owns opaque-handle lookup, status and expiry, connection-epoch currency, the inputResponses protocol shape, and journal-before-forward one-use consumption. The kernel checks the exact tool-and-arguments authorization target. Node tests project, server, continuation, expiry and response context before presenting that authorization state to the kernel. Therefore the accurate product claim is exactly: The authorization rule is TESTED (test/approval-contract.test.cjs and test/kernel-bridge.test.cjs). The state machine is TESTED.

The working Node loader does not use seal-config.js’s hard-coded demo-pk stub envelope. Protect stores an operator-signed config and pins its public key outside the envelope. The worker passes both to seal_init; it does not receive a private key. A state without a pin refuses authorization.

Before Protect, use the shipped contract/signed-policy.cjs module’s policyPayloads(selections) with the same tool selections planned for Protect. It returns the exact guard and forward payload strings. Sign each string’s UTF-8 bytes with an operator-held Ed25519 key. Put each payload and its hex signature in an envelope of the form {"payload":"...","signature":"..."}. Put the two envelope JSON strings in one JSON file as guard and forward. Set SEAL_KERNEL_POLICY_FILE to that file and SEAL_KERNEL_PUBKEY to the raw 32-byte public key in hex, then run seal protect SERVER TOOL [TOOL...]. Protect checks both signatures and the exact tool rules before it records the pin. Changed rules need a new signed policy at a new Protect operation. The signing key stays with the operator.

Assurance lineage — Seal family architecture

Section titled “Assurance lineage — Seal family architecture”

Lean proof source: the archived seal-host proof reference at d1af738b1f17966a18d7f86c51392b5cd3b8b0a1 is the reader-facing index for the Lean proof properties stated in this section.

This diagram describes the Seal family product, not the Node CLI shipped by this repository.

One diagram, five roles: seal-host decision core (proven [seal-host], archived repository), enforcement (family design; its seal-host deployment is archived), receipt (evidence), conformance (historical; archived seal-host finite corpus; no current CI run), coverage (audits the policy). Solid arrows are the runtime path; dashed arrows are evidence and audit paths.

flowchart LR
    agent["AI agent\n(MCP client)"]
    human["Human approver\n(signed approval,\nexact target)"]
    tool["Real tool\nDB / API / service"]


    subgraph host["Enforcement — seal-host (Rust; glue is TCB)"]
        gw["Mediation boundary\n(gateway)"]
    end


    subgraph kernel["Decision core — proven [seal-host] in Lean 4 (seal-host)"]
        core["default-deny · exact-target approval\nsingle-use · expiry · non-bypass"]
    end


    agent -->|tool call| gw
    human -->|approval| gw
    gw -->|canonical request| core
    core -->|ALLOW / BLOCK| gw
    gw -->|exact approved bytes only| tool


    receipt["Decision receipt (v2)\nSHA-256 hashes, tamper-evident"]
    gw --> receipt
    receipt -.-> verify["seal verify — CLI\n(seal-assurance-kit;\nshared kernel wasm)"]
    receipt -.-> browser["seal-check — browser\nshared kernel wasm"]
    receipt -.-> rdiff["seal receipt-diff:\nauthorization-surface diff\nbetween two receipts"]
    verify -.-> action["seal-verify-action:\narchived historical fork;\nnot a supported CI gate"]


    conf["Historical conformance bridge:\nfinite corpus in archived seal-host;\nno current CI run produces it"] -.-> gw
    scan["Coverage — seal scan:\npolicy audit (uncovered tools,\nindistinguishable calls)"] -.-> gw


    demo["seal-live-demo:\narchived historical demo evidence,\nBLOCK vs bypass, replayable evidence"] -.-> receipt

What each box is (and what it is not)

Section titled “What each box is (and what it is not)”

Lean proof source: the archived seal-host proof reference at d1af738b1f17966a18d7f86c51392b5cd3b8b0a1 is the reader-facing index for the Lean proof properties stated in this section.

  • Decision core (seal-host, the repository holding its Lean source) — the seal-host rulebook. The seal-host kernel has machine-checked [seal-host] Lean 4 theorems: default deny, allow iff a live approval record matches the exact target, single-use, expiry, non-bypass. The seal-host kernel is proven [seal-host] — but this is a kernel claim, not a whole-system claim; that the record was minted by the human you think is a custody assumption (truth box), not a theorem.
  • Enforcement (seal-host) — the guard at the door. The Rust MCP host that routes every guarded call through the kernel and forwards only the exact approved bytes. The Rust glue is TCB (trusted, not proven); historical conformance testing in archived seal-host tied it to the proof over a finite corpus. No current CI run produces that bridge evidence.
  • Receipt — every decision emits a v2 receipt (normative spec: the host’s authorization decision schema §11) with derived SHA-256 hashes. Tamper-evident, not tamper-impossible. seal verify (CLI) and seal-check (browser) are two interfaces over a shared verification lineage, not two implementations that can be expected to catch one another’s faults: their current published artifacts use byte-identical kernel WASM and common receipt-format semantics. The archived seal-verify-action was derived from the CLI closure as a downstream-stricter fork; it is not a supported CI gate. Agreement between the current interfaces is useful conformance evidence, but a defect in shared kernel or format logic can make them agree on the same wrong answer.
  • Conformance (historical conformance bridge) — archived seal-host holds finite corpus evidence comparing its Lean model, native Rust host, and wasm output. No current CI run produces this bridge evidence. It is evidence over that corpus, not a universal theorem.
  • Coverage (seal scan) — audits a policy against a tool inventory: uncovered tools, redundant rules, calls the policy cannot distinguish.
  • Drift (seal receipt-diff) — field-level diff for supported kit and host receipt families, classifying differences as authorization-surface or minor after checking each receipt’s own hashes. Other families, including spine-v2 pairs, are refused. It reports change; it does not re-verify a seal.
  • Historical CI fork (seal-verify-action) — this repository is archived. Its stricter signed_config profile describes historical verification work; it is not a supported gate for current deployments.
  • Sufficiency (seal adequacy) — the prior question: do the committed fields carry enough information to identify the effect they authorize? A found collision indicts the field set itself — no implementation reading those fields can fix it. This check caught Seal’s own pre-v2 approval surface; v2’s args_hash closes it.

Claim-status per box: CLAIMS-MATRIX.md. Honesty boundary: What Seal is NOT. Fleet links are public and resolve for everyone; collision-check is public.

Previous: Evaluator truth surface. Up: Assurance. Next: Distribution.