---
title: Stage 2 — Verification Subsystem
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---

← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]]  → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]]

# Stage 2: Verification Subsystem

*Summary: A verified gate evaluates every action against formal policy.
Capability-based authorization. "Root" as an attack target no longer exists.*

## What is added

- [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][ACL2-verified]] gate functions that evaluate every proposed action
- [[id:c34940cc-090e-57c4-8020-e78b1d32b96c][Capability-based authorization]]: every action requires a token, not an identity
- [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][Gate]] checks every action — from user, agent, or external message — against:
  - Is the action authorized by policy?
  - Does the capability grant this operation?
  - Does the action violate any system invariant?
- Decision procedure formalized in ACL2, machine-checked
- Gate runs as a decision layer on the conventional host (Stage 0 [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware]])
- **Provenance store becomes operational infrastructure:** a structured data extension of the Knowledge subsystem storing empirical parameters, validity envelopes, and benchmark results with full provenance chains
- **Validity envelope predicates as gate vectors:** the gate checks not only security policy but also scientific validity — is this model valid in this context? Are the parameters within their validated range? Does the input fall within the model's training distribution?

## What is eliminated

- **Unauthorized actions** — even a fully compromised endpoint cannot perform an
  action the gate blocks. The gate is the final arbiter, not the OS or client.
- **Privilege escalation** — no amount of subversion below the gate can grant
  capabilities the policy doesn't allow. The gate checks capability tokens,
  not caller identity.
- **"Root" as a meaningful attack target** — there is no root in Passepartout. There
  are capabilities, and capabilities are checked.

## What does this cost?

- **Verification latency** — every action is checked against policy. Complex
  policies add delay
- **Policy formalization burden** — everything must be written explicitly. Gaps
  block legitimate actions (false positives) or allow undesirable ones (false
  negatives). There is no [[id:4a1f23b0-abc8-4def-9876-543210abcdef][Common Sense]] fallback — the policy cannot rely on
  unformalized human intuition. Everything must be written down
- **Capability management complexity** — distributing, revoking, auditing
  capabilities is itself security-critical. A leaked capability is
  indistinguishable from an authorized action
- **Policy drift** — as the system evolves, the policy must evolve with it.
  Out-of-date policy blocks new legitimate uses
- **Proof maintenance** — the gate's decision procedure is verified, but the
  policy is not. Each policy change needs new proof
- **The gate runs on untrusted hardware** — if the OS or hardware is
  compromised, the gate's guarantees are meaningless. The attacker can skip
  the gate or modify its output. Full gate guarantees arrive at Stage 3

## What does this enable?

The system can now say "no" to unauthorized actions even when the endpoint is
fully compromised. Security is no longer dependent on client integrity. This is
the first layer where deductive guarantees enter the picture — but they are
contingent on Stage 3's trust substrate.

## When is this viable?

Today as a software layer on conventional hardware, but with limited guarantees
(the gate itself can be compromised by the host OS). Full power arrives at
Stage 3 when the gate runs on the verified Lisp machine.

## In practice

The gate is the final arbiter, not the OS or the client. But it runs on a
machine it doesn't trust. Users must weigh the benefit (unauthorized actions
blocked) against the operational cost (everything must be explicitly authorized
in policy). For high-stakes environments, the trade-off is worth it. For casual
use, the friction may lead users to bypass the gate.

*Full gate guarantees arrive when Passepartout runs on its own Lisp machine
(Stage 3). Before that, it's a correctness proof running on an untrusted substrate.*

← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]]  → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]]

:PROPERTIES:
:CREATED:  [2026-05-24 Sun]
:ID:       4a1f23b0-abc3-4def-9876-543210abcdef
:END:
