hermes-brain/projects/passepartout/architecture/architecture.org

Architecture

The project index introduces the case for verification and why it requires a uniform semantic model at hardware granularity. This page describes the architecture in detail: how the three subsystems fit together, how the gate works, what the Lisp machine looks like, and why the stack compresses into a single address space.

The gate as the central primitive.

The verification subsystem is a gate: a function that takes (action, context, policy) and returns (permit | deny). Every action passes through it — a shell command from the user, a proposal from the LLM, a message from the network, a file write by a scheduled job. There is no privileged path around the gate. There is no "run as root" because root is not a concept in the gate model — root is a convention enforced by an OS that the gate replaces.

The gate combines two decision layers:

1. ACL2-verified decision procedures for security-critical checks — access control, message authentication, capability resolution. These are provably correct for their domain.
2. An LLM for natural-language reasoning — parsing the user's intent, evaluating whether an action falls within policy boundaries that require human judgment.

The LLM layer is probabilistic. The ACL2 layer is deductive. The gate architecture ensures that the deductive layer is authoritative where it applies and the probabilistic layer is bounded by it — the LLM cannot overrule a verified denial.

The environment subsystem: one address space.

The environment eliminates the layered trust model of a conventional OS by eliminating the layers. Instead of an editor that sends keystrokes through a terminal emulator to a shell that forks processes that read files through a kernel VFS layer — each boundary a potential vulnerability — the environment subsystem runs everything in a single Lisp address space.

What this means concretely:

• The editor is a Lisp function that manipulates text buffers in the evaluated memory graph.
• The shell is a Lisp read-eval-print loop that compiles to the same evaluator.
• The browser renders HTML through a Lisp-based rendering engine, not through a separate browser process.
• The agent runtime invokes Lisp functions, not subprocesses.

(The specific implementations that realize this today use Lish for the shell and editor, Nyxt for the browser, and SBCL as the host Lisp — but the architectural principle is uniform semantics in one address space, not these particular packages.)

There is no MMU boundary between components because there are no separate processes. There is no IPC because there is nothing to communicate between — everything shares the same memory graph. The distinction between tool and self dissolves: your editor buffer, your shell history, your agent's state, and your social protocol messages all live in the same evaluated object graph, protected by the same gate, verified by the same prover.

The social protocol: provable communication.

The social protocol extends the verified semantics beyond a single machine. It provides:

• Self-sovereign DID identity (every instance has a cryptographic identity it controls)
• DIDComm encrypted messaging (end-to-end encrypted, signed, DAG-tracked)
• Personal data stores (user-owned, gate-controlled)
• Relay network (asynchronous message delivery across trust boundaries)
• Compute marketplace (provision verified the compute you rent)
• Liquid democracy (delegable voting over protocol governance)

Every message is signed by the sender's DID, tracked in a content-addressed DAG, and optionally notarized. Communication is provable when you choose it to be — you can prove what you sent, to whom, when, without revealing content.

The social protocol is not a blockchain. It uses DAG-based ordering for causality, not global consensus. Delegable trust replaces proof of work.

The staged progression.

The full architecture — gate-verified Lisp machine on custom silicon — is the destination. The staged roadmap describes how each successive replacement eliminates a class of threat:

• Stage 0: Conventional Linux, Python agent (Hermes), SQLite knowledge store (gbrain). The starting point. Zero days exist; patches are manual.
• Stage 1: Message-level authentication via the social protocol. Communication becomes provable.
• Stage 2: The gate operates as a software layer over the host OS. Shell commands, LLM proposals, and network messages all pass through the same decision procedure. Root is eliminated as an attack path.
• Stage 3: The host OS is replaced by a bare-metal SBCL image. The Lisp machine emerges. One address space, one evaluator, no MMU to attack.
• Stage 4: LLM inference moves into the Lisp process. No API calls across a network boundary. The LLM becomes a function in the same evaluated graph.
• Stage 5: Neural weights are stored as plist-native data structures. The gap between symbolic and neural representations closes.
• Stage 6: Verified fine-tuning. Every weight update is gate-checked against policy — the LLM cannot learn to bypass the gate because the gate is not in the LLM's mutable space.
• Stage 7: What remains. Physical theft, electronic warfare, holes in the specification itself, and the fallibility of the LLM oracle. These are limits of computation, not of this design.

Each stage is independently useful. Stage 0 is running today. The migration is progressive component swap, not a cut-over.

Downstream effects.

When every action is gate-checked, every message is provable, and every computation runs on verified semantics, the security model shifts from empirical to deductive. The downstream effects cascade beyond personal computing:

• Compliance becomes executable gate rules instead of annual audits. A SOC 2 report is a gate configuration, not a PDF.
• AI safety becomes a verified gate between the LLM and the action stream instead of probabilistic guardrails or RLHF.
• Software certification becomes the accumulated regression suite of every deployed instance — the Underwriters Laboratory for AI.
• Operating systems become obsolete. The gate replaces the kernel, the address space replaces process isolation, and the verified evaluator replaces the entire privilege model.